Curry-Howard Correspondence — Brief ☧

"In whom are hid all the treasures of wisdom and knowledge."

— Colossians 2:3 (KJV)

Q: Here is a surprising question. When you write a function that

takes an integer and returns a string, you probably think of it as

"processing data." But what if someone told you that the mere existence

of that function is also a proof of something? That sounds strange —

how can code be a proof?

A: This is the Curry-Howard correspondence, one of the most

profound connections in computer science. The idea is:

A type is a proposition (a statement that might be true or false)

A program of that type is a proof that the proposition is true

Type checking is proof verification

Let us make it concrete. The type Rain -> WetGround is the proposition

"if it rains, then the ground is wet." A function with that type is a

proof: given evidence of rain, it produces evidence of wet ground. If

you can write the function and it type-checks, you have proved the

implication.
Proposition:  "If it rains, the ground is wet"
Type:         Rain -> WetGround
Proof:        A function that, given evidence of rain,
              produces evidence of wet ground.
Q: So if I cannot write a function of some type, does that mean the

proposition is unprovable?

A: Precisely. If a type is uninhabited — meaning no value of that

type can ever be constructed — the corresponding proposition has no proof.

For example, there is no honest function of type Int -> Void (where

Void is the empty type with no values), because you can never produce

a Void. That corresponds to the logical fact that you cannot prove

"false" from an arbitrary integer.

On the flip side, Void -> a (from nothing to anything) is

trivially provable. Since there are no Void values, the function

never needs to actually run. This is the logical principle *ex falso

quodlibet* — from falsehood, anything follows.

Q: This is elegant, but does it have practical consequences?

A: Absolutely. It means a sufficiently powerful type system is also

a logic system. Languages like Agda, Idris, and Coq lean into this:

you write programs and prove theorems in the same language. Even in

everyday programming, when the compiler says "this type-checks," it is

telling you that a certain logical property holds about your code.

The Dictionary

Logic	Types	Programs
Proposition	Type	—
Proof	Value	—
Implication A → B	Function type `A -> B`	Lambda abstraction
Conjunction A ∧ B	Product type `(A, B)`	Pair construction
Disjunction A ∨ B	Sum type `Either A B`	Tagged union
True	Unit `()`	Trivial value
False	Void (empty type)	No constructor
∀x. P(x)	`forall a. P a`	Polymorphic function

This correspondence table is worth memorizing, because it will change how you think about programming. Every time you write a function, you are constructing a proof. Every time the compiler type-checks your code, it is verifying a logical argument. A pair (A, B) is evidence that both A and B are true -- a conjunction. An Either A B is evidence that at least one of A or B is true -- a disjunction. And polymorphism (forall a. P a) is a universal statement: the function works for every type, which means the proof works for every proposition of that form. Once you see this correspondence, types stop being mere annotations and become statements about what your code guarantees.

Connection to our project: miniKanren's search is proof search. When the

solver finds an answer -- say, that appending [1, 2] to [3] produces [1, 2, 3] -- it has constructively proved that the answer satisfies

all constraints. It did not merely check a candidate; it produced the witness (the proof term) through a sequence of unifications, each of which is a step in a logical derivation. Our FPGA accelerates

this proof search by performing constraint propagation over

Boolean domains at 770,000 operations per second, and each successful result is a

valid proof in the Curry-Howard sense. The bitmask domain represents the space of possible proofs; constraint propagation eliminates impossible proofs; and the final result is a constructive witness that the constraints are satisfiable. In this light, our entire system is a hardware-accelerated proof engine.

Learn more in the deep version

Related: Category Theory | Type Classes | Abstract Interpretation

Soli Deo Gloria