A Gentle Introduction to Curry–Howard

Q: What is the Curry–Howard correspondence

The Curry–Howard correspondence is the discovery that logic and computation share the same structure. A proposition corresponds to a type, a proof to a program (term) of that type, and proof reduction to computation (running the program). Summarized as 'proofs = programs, propositions = types,' it is the theoretical backbone of type-theory-based proof assistants such as Coq, Lean, and Agda.

Q: What does 'a proof is a program' mean concretely

A proof of 'if A then B' ($A \to B$) corresponds to a procedure that takes a proof of $A$ and returns a proof of $B$ — that is, a function of type $A \to B$. A proof of 'A and B' corresponds to a pair of a proof of $A$ and a proof of $B$. Building a proof is literally building a program.

Q: Why does the Curry–Howard correspondence matter

Through this correspondence, writing a proof and writing a program become the same, and type checking becomes proof checking. If you can construct a well-typed program, the proposition is proved, and a computer can guarantee the proof's correctness by mechanically checking the type. It is the very reason type-theory-based proof assistants are possible.

Propositions = types, proofs = programs

Introduction (high school to first-year university)

Goal of this page

Grasp the intuition of the Curry–Howard correspondence, that logic and computation share the same structure. Take a bird's-eye view of "propositions are types, proofs are programs, reduction is computation," and survey the backbone of this field at the outset.

1. Where logic and computation meet

In the previous chapters we saw a proof as "symbol manipulation that applies rules from axioms to reach a conclusion." Computation, on the other hand, is "running a program according to rules (reduction)." In the mid-20th century, it was discovered that these two have exactly the same structure. This is the Curry–Howard correspondence.

Definition: the Curry–Howard correspondence

The following correspondence between logic and typed computation: a proposition corresponds to a type, a proof to a program (term) of that type, and proof reduction (normalization) to computation (running the program).

2. The table of correspondence

Listing what each logical concept corresponds to on the computation side reveals how broad the correspondence is.

Figure 1: The table of the Curry–Howard correspondence. Each construction on the logic side translates directly into a type or program on the computation side.

3. "If… then" is a function

The center of the correspondence is implication. To prove "if $A$ then $B$" is nothing other than to show "a way to build a proof of $B$ given a proof of $A$." That is exactly a function from an input of type $A$ to an output of type $B$.

Example: modus ponens is function application

Given a proof of $A \to B$ (a function $f$) and a proof of $A$ (a value $a$), you obtain a proof of $B$. That is exactly function application $f(a)$. The logical inference rule "modus ponens" corresponds to the computational operation "pass an argument to a function."

$$\dfrac{A \to B \qquad A}{B} \quad\longleftrightarrow\quad f : A \to B,\ a : A \ \Rightarrow\ f(a) : B$$

Likewise, a proof of $A \land B$ corresponds to "a pair of a proof of $A$ and a proof of $B$," and a proof of $A \lor B$ to "a tagged proof recording which side was proved." Each logical connective becomes a familiar data structure from programming.

4. Why this is the field's backbone

Under the Curry–Howard correspondence, type checking is itself proof checking. If you can write a well-typed program, you have proved the corresponding proposition. Since a computer can check types mechanically, it can also guarantee the proof's correctness.

The principle of proof assistants

Proof assistants such as Coq, Lean, and Agda implement this correspondence. The user states a proposition (a type) and constructs a term (a proof = a program) of that type. The system confirms the proof's correctness by type checking. "Writing a proof" and "writing a well-typed program" become literally the same task.

The full foundation of this correspondence is treated in the λ-calculus (the computation side) and type theory (the type side). Extending the correspondence to include the quantifiers $\forall, \exists$ leads to dependent type theory, the source of the expressive power of Coq and Lean. For now, at the introductory level, it is enough to take home the bird's-eye view that "logic and computation are two faces of the same thing."

Summary

Key points

Curry–Howard correspondence: propositions = types, proofs = programs, reduction = computation
Implication $A \to B$ is a function type, conjunction $A \land B$ a pair, disjunction $A \lor B$ a sum
Modus ponens corresponds to function application $f(a)$
Type checking = proof checking. This is the backbone of type-theory-based proof assistants
The correspondence deepens through the λ-calculus, type theory, and dependent type theory

Frequently asked questions

What is the Curry–Howard correspondence?

The discovery that logic and computation share the same structure. A proposition corresponds to a type, a proof to a program (term) of that type, and proof reduction to computation. Summarized as "proofs = programs, propositions = types," it is the backbone of type-theory-based proof assistants such as Coq, Lean, and Agda.

What does "a proof is a program" mean concretely?

A proof of "if $A$ then $B$" ($A \to B$) corresponds to a procedure that takes a proof of $A$ and returns a proof of $B$ — a function of type $A \to B$. A proof of "$A$ and $B$" corresponds to a pair of a proof of $A$ and a proof of $B$. Building a proof is building a program.

Why does the Curry–Howard correspondence matter?

Writing a proof and writing a program become the same, and type checking becomes proof checking. If you can construct a well-typed program, the proposition is proved, and a computer can guarantee correctness by checking the type. It is the very reason type-theory-based proof assistants are possible.