The Curry - Howard isomorphism and how to make your own formal proof verifier

As the cost of bugs and failures in systems increase as we rely more on code, the need to understand proof-checkers and formal verifiers is essential as we shift from a move-fast-and-break-things paradigm.

Here is my take on it, discussing how proof checkers leverage the Curry-Howard isomorphism and showing how to make a formal proof verifier yourself

https://timothysamson.github.io/posts/curry-howard/

3 Likes