Introduction

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:

Logic Programs
Proposition AA Type AA
Proof of AA Term of type AA
Implication A→BA \to B Function type A→BA \to B
Conjunction A ∧ B Product type A×BA \times B
Disjunction A ∨ B Sum type A+BA + B
False (⊥) Empty type (no inhabitants)

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

Build a Typed Proof

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">Each <b>proposition</b> in the left column is a type. Each <b>λ-term</b> on the right is a program.
    Select one from each column, then click <b>Check</b> — if the term inhabits the type, you have produced a proof.</p>
<div class="cols">
  <div class="col">
    <div class="col-label">Proposition (Type)</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">λ-Term (Program)</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">left injection</span></button>
  </div>
</div>
<div class="selection">
  Selected: <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</button>
<button id="reset-btn" type="button" class="ghost">Reset</button>
<div class="result" id="result"></div>
<div class="legend">
  <b>Key:</b> A → B = "if A then B" = function type &nbsp;|&nbsp; A ∧ B = product type (pair) &nbsp;|&nbsp; A ∨ B = sum type (either)
</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; }

// Curry-Howard correspondence demo.
// Each proposition is a type; each term is a program.
// We hard-code a "type-checking" table: which (prop, term) pairs are valid proofs.
// The logic follows the simply-typed lambda calculus:
//   λx.x        : A → A             (identity / axiom)
//   λx.λy.x     : A → B → A         (const / weakening)
//   λf.λg.λx.g(f x) : (A→B)→(B→C)→A→C  (compose / cut / transitivity)
//   λp.fst p    : A ∧ B → A          (fst / left-projection / ∧-elimination)
//   λx.inl x    : A → A ∨ B          (left-injection / ∨-introduction-left)

const PROOFS = {
  // [proposition, term] => explanation
  'A → A|λx.x':
    '✓ λx.x has type A → A. The identity function proves "A implies A" — the simplest tautology.',
  'A → B → A|λx.λy.x':
    '✓ λx.λy.x has type A → B → A. Ignoring the second argument proves "if A, then B is irrelevant and A still holds" (weakening).',
  '(A → B) → (B → C) → A → C|λf.λg.λx.g(f x)':
    '✓ λf.λg.λx.g(f x) has type (A→B)→(B→C)→A→C. Function composition proves transitivity of implication.',
  'A ∧ B → A|λp.fst p':
    '✓ λp.fst p has type A ∧ B → A. Projecting the first component of a pair proves conjunction-elimination.',
  'A → A ∨ B|λx.inl x':
    '✓ λx.inl x has type A → A ∨ B. Injecting into the left branch proves disjunction-introduction.',
};

const WRONG_TERM = {
  'λx.x': 'λx.x has type A → A. It cannot prove this proposition because the output type must equal the input type.',
  'λx.λy.x': 'λx.λy.x has type A → B → A. Its result is the first argument, not what this proposition needs.',
  'λf.λg.λx.g(f x)': 'λf.λg.λx.g(f x) has type (A→B)→(B→C)→A→C. It requires two function arguments first.',
  'λp.fst p': 'λp.fst p expects a pair (A ∧ B) as its argument, not a single value.',
  'λx.inl x': 'λx.inl x produces a sum type A ∨ B, which does not match this proposition.',
};

let selProp = null, selTerm = null;

function setResult(text, cls) {
  const r = document.getElementById('result');
  r.textContent = text; r.className = 'result ' + cls;
}

document.querySelectorAll('.prop-btn').forEach(btn => {
  btn.addEventListener('click', () => {
    document.querySelectorAll('.prop-btn').forEach(b => b.classList.remove('active'));
    btn.classList.add('active');
    selProp = btn.dataset.prop;
    document.getElementById('sel-prop').textContent = selProp;
    setResult('', '');
  });
});

document.querySelectorAll('.term-btn').forEach(btn => {
  btn.addEventListener('click', () => {
    document.querySelectorAll('.term-btn').forEach(b => b.classList.remove('active'));
    btn.classList.add('active');
    selTerm = btn.dataset.term;
    document.getElementById('sel-term').textContent = selTerm;
    setResult('', '');
  });
});

document.getElementById('check-btn').addEventListener('click', () => {
  if (!selProp || !selTerm) {
    setResult('Select a proposition and a term first.', 'info'); return;
  }
  const key = selProp + '|' + selTerm;
  if (PROOFS[key]) {
    setResult(PROOFS[key], 'ok');
    console.log('PROOF:', key, '=> valid');
  } else {
    const hint = WRONG_TERM[selTerm] || 'This term does not have the selected type — no proof.';
    setResult('✗ ' + hint, 'bad');
    console.log('PROOF:', key, '=> invalid');
  }
});

document.getElementById('reset-btn').addEventListener('click', () => {
  selProp = null; selTerm = null;
  document.getElementById('sel-prop').textContent = '—';
  document.getElementById('sel-term').textContent = '—';
  document.querySelectorAll('.prop-btn, .term-btn').forEach(b => b.classList.remove('active'));
  setResult('', '');
});
Result
Console

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

How Deep Does It Go?

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. VecnVec n for a vector of exactly nn 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 AA or a proof of BB. 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.

Where It Matters

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→Aidentity : A \to A, they are, without knowing it, writing the axiom "A implies A" in disguise.

Conclusion

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.

Share this article

Pick a channel — or use your device's native share sheet.

Comments

Loading comments...

https://www.kipuhub.com/en/article/curry-howard/Content licensed under CC BY-NC 4.0.