Field note

Curry–Howard: A Theorem Is a Type, and Its Proof Is a Program

Mathematical Foundations

Start with a physical picture. Treat every statement as a box. Proving the statement means putting an object of the required shape into the box.

A proof of A and B contains evidence for both: a pair (A, B).
A proof of A or B contains one value plus a tag saying which case: Either<A, B>.
A proof of A implies B is a machine that turns any evidence for A into evidence for B: a function A -> B.
False is an empty type: a box with no possible value.

This is the Curry–Howard correspondence. A proposition is a type, a proof is a value of that type, and checking a proof is type-checking the value.

“There exists” contains the answer

The statement “there exists an even number” is not satisfied by reassurance. Its proof contains a number and evidence that it is even. In dependent-type notation it is a pair:

(n : Nat) × Even(n)

“For every n, there exists an even m at least as large” has a different shape. One fixed pair cannot answer every input, so the proof must be a function:

(n : Nat) -> (m : Nat) × Even(m) × (m >= n)

The implementation can return 2 × n, together with the arithmetic evidence. Remove the proof fields and an algorithm remains. A constructive proof of a for-all/there-exists theorem is software with its specification welded to it.

Euclid as an executable proof

“There are infinitely many primes” can be stated constructively as:

(n : Nat) -> (p : Nat) × Prime(p) × (p > n)

Given n, multiply the integers from 1 through n, add one, and choose the smallest non-trivial factor p. That factor is prime: otherwise it would have a smaller factor. It is greater than n: every integer from 2 through n divides the product, so dividing the product-plus-one by any of them leaves remainder one.

Running the proof produces a prime above the input. A different proof of the same type may use a better algorithm, but the type preserves the guarantee while the implementation changes.

Why this matters to a resource vault

The correspondence encourages specifications that exclude illegal programs. A sealed Open | Claimed type makes every state-dependent field explicit. A transition function must cover each case. Linear logic goes further: evidence cannot be silently copied or dropped, matching a resource system in which value must be consumed once and completely accounted for.

There is one important boundary. A proof term checked by a type system is not the same object as a cryptographic zero-knowledge proof. They meet when we prove that a circuit implements its specification: the circuit proof protects one execution, while the type-level or formal proof protects the meaning of the circuit itself.

See the two-state resource type → · Read about completeness →