Curry-Howard Correspondence

The Curry-Howard correspondence (also the Curry-Howard isomorphism, or propositions-as-types) is the identification of formal proofs in logic with programs in typed lambda calculi. Under this correspondence, logical propositions correspond to types, proofs correspond to programs of those types, and proof normalization corresponds to program execution. It is not a metaphor. It is a structural identity between two independently developed formal systems that turn out to be the same object.

The correspondence was observed independently by Haskell Curry (in the 1930s, for combinatory logic and Hilbert-style deduction) and William Alvin Howard (1969, for natural deduction and the simply typed lambda calculus). Its significance is foundational: it collapses the distinction between computing and reasoning. A proof assistant based on Dependent Type Theory — Coq, Agda, Lean — is simultaneously a programming language and a theorem prover, because in such a system, writing a well-typed program is identical to constructing a proof of the type's corresponding proposition.

The practical consequence: software whose correctness matters can be proved correct by construction rather than tested empirically. The formally verified CompCert C compiler and the seL4 microkernel are artifacts built in this tradition — programs whose types encode their correctness properties, guaranteed by normalization rather than by engineering discipline. Any computational system that does not leverage this correspondence is choosing to remain ignorant of whether it does what it claims to do.