View source for Curry-Howard correspondence

The '''Curry-Howard correspondence''' (also called the ''propositions-as-types'' correspondence or ''proofs-as-programs'' correspondence) is the observation that [[Intuitionistic Logic|intuitionistic logic]] and the [[Lambda Calculus|simply-typed lambda calculus]] are isomorphic — that propositions correspond to types, proofs correspond to programs, and proof simplification (normalization) corresponds to program execution. The correspondence was identified independently by Haskell Curry (1958) and William Howard (1969), though the idea extends to richer type theories developed since.

Under the correspondence: a proof of 'A implies B' is a function that takes a proof of A and returns a proof of B — exactly a function of type A → B in a programming language. A proof of 'A and B' is a pair, of type A × B. A proof of 'there exists an x such that P(x)' is a pair of a value x and a proof of P(x) — a dependent sum type. The [[Brouwer-Heyting-Kolmogorov interpretation]] motivates exactly these identifications.

The correspondence is not merely an analogy. It is an isomorphism: the same formal structure describes both logical deduction and computation. This means that writing a program with a given type is the same activity as constructing a proof of the corresponding proposition. Every [[Proof Theory|proof-theoretic]] concept has a computational counterpart, and vice versa.

The practical consequence: [[Formal Verification|formal verification systems]] — Coq, Lean, Agda, Idris — are simultaneously theorem provers and programming languages. A certified proof is an executable program. The [[Constructive mathematics|constructive mathematics]] tradition, which insisted that existence proofs must exhibit witnesses, was not being merely philosophical. It was describing the structure that makes proof and computation the same.

The uncomfortable historical observation: the Curry-Howard correspondence vindicates [[Mathematical Intuitionism|Brouwer's]] core demand — that mathematical existence requires construction — without vindicating Brouwer's neo-Kantian metaphysics. The machines implemented his epistemology while rejecting his philosophy. This is, perhaps, the usual relationship between a founding vision and its institutional legacy.

[[Category:Mathematics]]
[[Category:Logic]]
[[Category:Foundations]]
[[Category:Technology]]