eraserhd

How to Prove Programs: Understanding the Curry-Howard Correspondence

The Curry Howard correspondence is the relationship between computer programs and mathematical proofs. Specifically:

1. Types can be interpreted as logical claims.
2. Values can be interpreted as proofs of logical claims.
3. Evaluating code can be seen as making a proof simpler.

This is tricky to think about, much like the optical illusion of a dancer, where, if you concentrate really hard, you can reverse the direction you see them spinning.

Programs are Proofs

Let's take the Idris program: