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 and the 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-theoretic concept has a computational counterpart, and vice versa.

The practical consequence: formal verification systems — Coq, Lean, Agda, Idris — are simultaneously theorem provers and programming languages. A certified proof is an executable program. The 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 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.