Approaches to Data-Driven Verification

It is desirable to verify (that is, to prove the correctness of) many systems. Here, I explain some of the techniques and terminology involved in verification. No proof assistant is used, but all mathematics are done in a way that it could trivially be translated to any system based on constructive type theory.

see more

Sigma, Pi. Sum, Product.

On my earliest expeditions into the world of type theory, I remember being very irritated by the apparent inconsistency in the naming of (dependent) sum and product. After exploring a little more, my confusion disappeared, and irritation gave way to appreciation for the (actual) symmetries that those names express. Here, I'll explain this symmetry using some simple examples, and in the process hopefully give a tolerable introduction to dependent types for curious newcomers.

see more

Literate Theorem Proving with Org

Recently, I've been messing around with Coq. Despite having experience with similar dependently-typed languages/theorem-provers like Agda and Idris, I was intimidated by Coq's "weird" (read: not Haskell-like) syntax and pretty much paid it no attention for a few years. However, I've been increasingly frustrated with the tooling for those languages, which tends to be undocumented and buggy. The situation with Coq, which as far as I know is much more commonly used, seems to be better. Here, I won't focus so much on the language itself but rather on my editor configuration and workflow.

see more

Author: Samuel Breese

Created: 2019-10-15 Tue 19:57