Curry–Howard — proofs are programs
Parent: logic
The hinge of the whole branch: propositions = types, proofs = programs, proof-normalization = computation. Logic and computation are the same structure seen twice.
The dictionary
| logic | type theory / programming |
|---|---|
proposition A | type A |
proof of A | program (term) of type A |
A → B (implies) | function type A → B |
A ∧ B | product A × B (pair) |
A ∨ B | sum A + B (tagged union) |
⊤ / ⊥ | unit / empty type |
∀x.P(x) | dependent function Π(x:A). P x |
∃x.P(x) | dependent pair Σ(x:A). P x |
| cut / detour elimination | β-reduction (evaluation) |
A proof that assumes A and derives B is literally a function turning evidence-for-A into evidence-for-B. Checking a proof = type-checking a term.
Why it's deep, not a pun
- Constructivity: to prove
∃x.P(x)you must build a witnessxand a proof ofP(x)— i.e. a program producing them. So intuitionistic logic ⟺ typed λ-calculus exactly (classical logic needs control operators — Griffin 1990,call/cc). - Normalization = running: cut-elimination (simplifying a proof) is β-reduction (evaluating a program). A normalized proof is a value.
- History: Curry (combinatory logic, 1930s–58), Howard (1969) "formulae-as-types," de Bruijn (Automath). It's why machine proof is even possible.
Consequence
You can compute with proofs and verify programs as proofs. This is the foundation of proof assistants: dependent type theory gives types rich enough to be any proposition, and Lean 4 checks proofs by type-checking. From computation and proof, one object.