The Curry–Howard Correspondence

Here is one of the most beautiful facts in all of computer science, and it sounds too good to be true: a logical proof and a computer program are the same thing. Not "analogous", not "similar in spirit" — literally the same mathematical object, viewed through two lenses. A proof of a theorem is a program; the theorem it proves is that program's type; and running the program is simplifying the proof. This is the Curry–Howard correspondence (also called the proofs-as-programs, or propositions-as-types, principle).

Haskell Curry noticed the shape of the coincidence in the 1930s–40s; William Howard wrote it out in full in 1969. It ties together three worlds you have met separately — the proof systems of logic, the lambda calculus of computation, and the type systems of programming — and shows they were one world all along.

The core slogan, in three parts

The first consequence is startling: because a well-typed term is a proof, a type checker is a proof checker. If your program compiles at type A, you have a machine-verified proof of the proposition A. The connection to type safety is now transparent — soundness is what makes the type-checker-as-proof-checker trustworthy.

The dictionary

The correspondence is a precise, connective-by-connective dictionary between logic and types. Learn this table and you can translate any statement in one column into the other:

LogicTypes / programsReading
Implication A \Rightarrow B Function type A \to B A proof of A \Rightarrow B is a function turning a proof of A into a proof of B.
Conjunction A \wedge B Product / pair A \times B To prove "both", give a pair: a proof of each.
Disjunction A \vee B Sum / tagged union A + B To prove "either", give a tagged choice saying which side you proved.
Truth \top Unit type \mathbf{1} Trivially provable — the empty tuple () inhabits it.
Falsehood \bot Empty type \mathbf{0} No proof, no value — the type with no inhabitants.
Negation \neg A A \to \mathbf{0} A proof of \neg A turns a proof of A into absurdity.
Universal \forall x.\,P(x) Dependent function \prod_{x} P(x) A function whose result type depends on the input value.
Existential \exists x.\,P(x) Dependent pair \sum_{x} P(x) A witness value paired with a proof it has the property.

A worked translation

Take the tautology A \wedge B \Rightarrow A — "if both hold, then the first holds." Under the dictionary this proposition is the type A \times B \to A, and a proof of the tautology is a program of that type. Which program? The one that takes a pair and returns its first component:

// Proposition: A ∧ B ⇒ A // Type: [A, B] -> A // Proof/program: project out the first component. function proof<A, B>(both: [A, B]): A { return both[0]; } // Proposition: A ⇒ (B ⇒ A) ("a true thing follows from anything") // Type: A -> (B -> A) const k = <A, B>(a: A) => (b: B): A => a; // return a, ignore b

Read proof as a derivation: "assume a proof both of A \wedge B; by \wedge-elimination take the left part; that is a proof of A." The program is that derivation. And k is the proof of A \Rightarrow (B \Rightarrow A) — which logicians call an axiom and combinator theorists call the K combinator. Same object, two names.

It removes detours. In natural deduction, a "cut" is a wasteful step where you prove a lemma and immediately use it — introduce a connective, then eliminate it right away. Normalising the proof (cut-elimination) splices the lemma's proof directly into where it's used. On the program side that detour is exactly a redex: (\lambda x.\,e)\,v — build a function, then apply it — and \beta-reduction substitutes v in for x, splicing the argument's value into the body. Cut-elimination in logic and evaluation in the lambda calculus are the very same process. A fully-evaluated program corresponds to a proof in normal form — one with no detours left.

Dependent types give you predicate logic — and proof assistants

Simple types (with \to, \times, +) match propositional logic. To reach full first-order logic — statements with \forall and \exists quantifying over values — you need dependent types, where a type may mention a value. Then \forall becomes a dependent function type (the return type depends on the argument) and \exists a dependent pair (a witness plus a proof about it). Predicate logic and dependently-typed programming are two faces of one coin.

This is the engineering payoff. A proof assistant — Coq, Lean, Agda — is a programming language with dependent types in which you write proofs as programs and the type checker verifies them. When Georges Gonthier's team machine-checked the Four Colour Theorem, or when the Feit–Thompson theorem was formalised in Coq, the "proof" was a program the type checker accepted. Software verified this way (the CompCert C compiler, the seL4 microkernel) carries a correctness guarantee as strong as a mathematical theorem — because, by Curry–Howard, it is one.

The clean dictionary holds for intuitionistic (constructive) logic, not classical logic. The reason is built into "proofs are programs": to prove A \vee B you must supply a tagged value saying which side holds — you cannot prove a disjunction without knowing a disjunct. So the classical law of excluded middle, A \vee \neg A, has no program: there is no computable function that, for an arbitrary proposition, returns a proof of it or a proof of its negation (that would decide the undecidable). Likewise double-negation elimination \neg\neg A \Rightarrow A is not constructively provable — knowing "not not A" gives you no witness for A. You can recover classical logic by adding these as axioms (or, wonderfully, via control operators like call/cc — Griffin's discovery), but the plain, pure correspondence is constructive. Assuming excluded middle "for free" is the classic slip.