A proof and a program are not analogous — they are the same object, read twice. A proposition is a type; a proof is a term of that type; proof-simplification is evaluation. Down the center, data flows: a proposition goes in, the type-checker decides, an inhabiting program comes out. The blue team builds the checker; the red team pairs a proof with the wrong type to break the isomorphism.
source W. A. Howard, "The Formulae-as-Types Notion of Construction" (privately circulated 1969; published 1980) — in To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press, pp. 479–491. No stable DOI — scanned copy. Rendered, not quoted.
Each natural-deduction rule is a term constructor; checking a proof is type-checking a program. The blue team implements one type-checker; it decides every proof at once.
| rule | term |
|---|---|
| →I (implication intro) | λx:A. e |
| →E (modus ponens) | (f a) — application |
| ∧I (conjunction intro) | ⟨a, b⟩ — pair |
| ∧E (conjunction elim) | fst e / snd e |
| ∨I (disjunction intro) | inl e / inr e |
| ∨E (disjunction elim) | case e of … |
Selected proof-term, type derived live by the checker:
This sphere is the bridge from the-natural-deduction to the-simply-typed-lambda-calculus. Gentzen's proof rules and Church's typed terms turn out to be one system: a proof checked by a logician is a program checked by a type-checker.
Take a proof out of the left sphere, read its rules as constructors, and it lands as a term in the right sphere with no gap. Each sphere is the next one's premise — here the premise is that deduction and typing are the same act.
The blue team's live check: re-run the type-checker and the intuitionistic decision procedure over the whole corpus and confirm provable ⇔ inhabited. If red mislabels a proof, this badge catches it.
Feed the machine a proposition. The correspondence reads it two ways at once — as a claim in logic, and as a type in a programming language. The dictionary is exact:
| logic (proposition) | program (type) | a proof is… |
|---|---|---|
| A → B implication | A → B function | a λ, used by application |
| A ∧ B conjunction | A × B product | a pair ⟨a,b⟩, used by fst/snd |
| A ∨ B disjunction | A + B sum | inl/inr, used by case |
| A assumption | x : A | a variable |
Same structure, two readings. That is the whole correspondence — and it is what you feed the panel below.
The checker runs live: it type-checks the proof-term and, independently, decides provability by a contraction-free sequent search (Dyckhoff G4ip). Nothing is looked up.
What the machine produces, proven: for each provable proposition a well-typed program whose type equals the proposition (proofs = programs); for each unprovable one, an empty type — no closed term inhabits it. The identity proof of A→A is exactly the identity function λx. x, and modus ponens is exactly application.
The blue witness (left) re-checks provable⇔inhabited live; the red team (right) tries to make a proof-term claim the wrong type.
This panel is also only propositional: no quantifiers, so no dependent types. First-order ∀/∃ needs ∏/∑ types (Martin-Löf), which this checker does not implement. And consistency of the logic rests on strong normalization of the calculus — assumed here, not proved on-page.
"Curry and Howard proved it together." Cut. Curry noted the combinator/axiom fit in the 1930s–50s; Howard extended it to natural deduction and full λ-calculus in a 1969 note, published 1980. Two people, decades apart.
"A proof is like a program." Cut. Not like — it is one, up to notation. The checker below type-checks the very term that is the proof; there is no translation step.
"Every type is inhabited (just write some code)." Kept, corrected. A type is inhabited iff its proposition is provable. A and A→B have no closed inhabitant — the decision procedure proves it.
The red team's move: pair the identity proof λx. x (which really proves A→A) with the wrong type A→C. If the correspondence were loose, the mislabel would slide by.
Claim the wrong type and two things fail at once: the type-checker still derives A→A (≠ A→C), and A→C is not provable — so provable⇔inhabited breaks and the witness (window 7) turns red. Nothing is faked; the attack is real and it is caught.