The Curry-Howard Correspondence

In 1934, logician Haskell Curry noticed something odd: the types of combinators in combinatory logic matched the axioms of intuitionistic logic. Twenty years later, William Howard formalized the observation for the λ-calculus — and the Curry-Howard correspondence was born.

The correspondence states three things at once:

• A proposition in logic is exactly a type in a programming language.
• A proof of a proposition is exactly a program of that type.
• Simplifying a proof (normalizing it) is exactly running a program.

This is not a metaphor. It is a precise mathematical isomorphism — every construct on one side maps to a matching construct on the other:

The simplest instance: a function $f : A \to B$ is literally a proof that "if $A$ then $B$". Calling $f$ on a proof of $A$ produces a proof of $B$ — exactly modus ponens.

Select a proposition (logical statement) on the left, then choose a λ-term on the right. If the term's type matches the proposition, you have produced a proof. Click Check to verify.

<p class="hint">{{hint_intro}}</p>
<div class="cols">
  <div class="col">
    <div class="col-label">{{col_prop}}</div>
    <button class="prop-btn" data-prop="A → A">A → A</button>
    <button class="prop-btn" data-prop="A → B → A">A → B → A</button>
    <button class="prop-btn" data-prop="(A → B) → (B → C) → A → C">(A → B) → (B → C) → A → C</button>
    <button class="prop-btn" data-prop="A ∧ B → A">A ∧ B → A</button>
    <button class="prop-btn" data-prop="A → A ∨ B">A → A ∨ B</button>
  </div>
  <div class="col">
    <div class="col-label">{{col_term}}</div>
    <button class="term-btn" data-term="λx.x">λx.x &nbsp;<span class="tag">identity</span></button>
    <button class="term-btn" data-term="λx.λy.x">λx.λy.x &nbsp;<span class="tag">const</span></button>
    <button class="term-btn" data-term="λf.λg.λx.g(f x)">λf.λg.λx.g(f x) &nbsp;<span class="tag">compose</span></button>
    <button class="term-btn" data-term="λp.fst p">λp.fst p &nbsp;<span class="tag">fst</span></button>
    <button class="term-btn" data-term="λx.inl x">λx.inl x &nbsp;<span class="tag">{{tag_left_injection}}</span></button>
  </div>
</div>
<div class="selection">
  {{selected_label}} <span id="sel-prop" class="sel-item prop-color">—</span> &nbsp;≅&nbsp; <span id="sel-term" class="sel-item term-color">—</span>
</div>
<button id="check-btn" type="button">{{check_btn}}</button>
<button id="reset-btn" type="button" class="ghost">{{reset_btn}}</button>
<div class="result" id="result"></div>
<div class="legend">
  <b>{{legend_key}}</b> {{legend_body}}
</div>

* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; color: #222; margin: 0; padding: 4px; }
.hint { font-size: .88rem; color: #444; margin: 0 0 .8rem; line-height: 1.5; }
.cols { display: flex; gap: 1rem; flex-wrap: wrap; }
.col { flex: 1; min-width: 180px; display: flex; flex-direction: column; gap: .35rem; }
.col-label { font-size: .75rem; font-weight: 700; text-transform: uppercase; letter-spacing: .06em; color: #666; margin-bottom: .15rem; }
.prop-btn, .term-btn {
  font: 600 13px ui-monospace, monospace; padding: .45rem .7rem; border-radius: 8px;
  cursor: pointer; text-align: left; transition: all .12s; border: 1.5px solid #cdd9e3;
  background: #f0f4f8; color: #1d3557;
}
.prop-btn:hover { background: #dce8f5; }
.term-btn:hover { background: #e8f5e8; }
.prop-btn.active { background: #1d3557; color: #fff; border-color: #1d3557; }
.term-btn.active { background: #0a7d33; color: #fff; border-color: #0a7d33; }
.tag { font-size: .75rem; font-weight: 400; opacity: .8; }
.selection { margin: .8rem 0 .5rem; font-size: .9rem; min-height: 1.4em; }
.sel-item { font-family: ui-monospace, monospace; font-weight: 700; }
.prop-color { color: #1d3557; }
.term-color { color: #0a7d33; }
button { font: 600 14px system-ui, sans-serif; padding: .45rem .9rem; border: 1px solid #1d3557;
         background: #1d3557; color: #fff; border-radius: 8px; cursor: pointer; margin-right: .4rem; }
button.ghost { background: #fff; color: #1d3557; }
.result { margin-top: .7rem; font-size: 1rem; font-weight: 700; min-height: 1.5em; }
.result.ok { color: #0a7d33; }
.result.bad { color: #c92f3c; }
.result.info { color: #555; font-weight: 400; font-size: .9rem; }
.legend { margin-top: .9rem; font-size: .8rem; color: #555; line-height: 1.6; border-top: 1px solid #e0e5ea; padding-top: .5rem; }

// Code not found

Each successful match is an instance of the isomorphism: the program is the proof. Notice that $A \to A$ (identity) is always provable — and λx.x always inhabits it. A type with no term (like $A \to ⊥$) is an unprovable proposition in this fragment.

The basic correspondence covers simply typed λ-calculus and propositional logic. But it extends much further — and each extension is a genuine discovery about the structure of computation and mathematics.

Dependent types (where a type can depend on a value, e.g. $Vec n$ for a vector of exactly $n$ elements) correspond to predicate logic — the logic of "for all x, P(x)" and "there exists x such that P(x)". This is the foundation of proof assistants like Coq (Thierry Coquand, Gérard Huet, 1984) and Lean (Leonardo de Moura, 2013).

Classical logic vs. intuitionistic logic: the correspondence naturally lands in intuitionistic logic, where a proof of A ∨ B must explicitly produce either a proof of $A$ or a proof of $B$. Classical logic's law of excluded middle (A ∨ ¬A) has no computational content — adding it corresponds to adding control operators like call/cc (call with current continuation).

The Curry-Howard-Lambek correspondence extends the picture to category theory: propositions are objects, proofs are morphisms, and logical connectives are categorical constructions. Logic, computation, and algebra are three names for the same thing.

The status: proven correspondence (not open, not undecidable). Haskell Curry's 1934 observation + Howard's 1969 unpublished manuscript (published 1980) + decades of extensions by de Bruijn, Martin-Löf, Coquand and others have turned this into a rock-solid foundation. It is the working principle behind every modern proof assistant.

Compare this with P vs NP: there the gap between finding and checking is the mystery. In Curry-Howard the mystery dissolved — the gap between logic and programs vanished.

The Curry-Howard correspondence is not just a philosophical curiosity — it is the engineering principle behind a growing class of critical software tools.

• Proof assistants (Coq, Lean, Agda, Isabelle/HOL): users write programs that are simultaneously proofs. The Feit-Thompson theorem (255 pages of mathematics) was fully verified in Coq in 2012 by Georges Gonthier's team. The CompCert C compiler, also verified in Coq, has a mathematically proven guarantee that it never miscompiles a program.
• Dependently typed languages (Idris, Agda): types can express specifications — a function's type can say "this sort returns a list that is sorted and has the same elements as the input". The compiler then checks the proof.
• Homotopy Type Theory (HoTT): a 2013 synthesis connecting type theory to homotopy theory (topology), where types are spaces and proofs are paths. The Univalent Foundations program (Vladimir Voevodsky, Fields Medal) aims to rebuild all of mathematics on this foundation.
• Blockchain and smart contracts: formal verification tools for Ethereum contracts use Curry-Howard-inspired type systems to prove that a contract cannot overflow or re-enter unsafely.
• Compiler correctness: the halting problem tells us we cannot verify all programs automatically. But Curry-Howard gives us a way to write programs whose correctness is by construction — no separate verification step needed.

Every time a programmer writes a generic function $identity : A \to A$, they are, without knowing it, writing the axiom "A implies A" in disguise.

The Curry-Howard correspondence is one of the most beautiful results in the history of ideas. What began as Curry noticing a numerical coincidence in 1934 became a precise, proven isomorphism between mathematical logic and the theory of computation — two fields that had developed independently for decades.

The punchline is philosophical as much as mathematical: when you write a function, you are proving a theorem. When you prove a theorem, you are writing a program. The distinction was never real — it was just two communities using different words for the same object.

This has concrete consequences today: Coq, Lean, Agda and their cousins use this isomorphism to let mathematicians write machine-checked proofs and programmers write provably correct software. The correspondence keeps deepening — homotopy type theory hints that the story extends all the way to geometry.

Compared to open problems like P vs NP or the halting problem, Curry-Howard is a rare completed mystery. The bridge between logic and programs is not a conjecture — it is a theorem, and it holds all the way down.