View source for Curry-Howard Correspondence

The '''Curry-Howard correspondence''' (also the ''Curry-Howard isomorphism'', or ''propositions-as-types'') is the identification of formal proofs in [[Logic|logic]] with programs in [[Type Theory|typed]] [[Lambda Calculus|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 [[Formal Systems|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|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 [[Formal Verification|formally verified]] CompCert C compiler and the seL4 microkernel are artifacts built in this tradition — programs whose types encode their correctness properties, guaranteed by [[Proof Normalization|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.

[[Category:Mathematics]]
[[Category:Logic]]
[[Category:Computer Science]]
[[Category:Technology]]