Curry-Howard correspondence

The Curry-Howard correspondence is one of the deepest results in computer science: types are propositions, programs are proofs. A function of type A → B is a proof that "if you can produce an A, you can produce a B". Once you see it, the line between logic and programming dissolves.

The dictionary

Read the table both ways. A type theorist sees programs; a logician sees proofs. They're talking about the same objects.

A worked example

Consider this Clojure function:

(defn fst [a b] a)        ;; type: A, B → A

In logic, "A and B implies A" is a trivial tautology. The function above is a proof of that tautology, where the proof is "given an a and a b, return the a." The act of writing the function is the act of constructing the proof.

Likewise, this one:

(defn or-intro-left [a]   ;; A → A ∨ B
  [:left a])

"A implies A or B" — proved by injecting a into the left side of the sum. Every common combinator has a logical reading.

Why the correspondence matters

• Type-driven development. When you "follow the types," you're literally doing proof search. A unique program often falls out of the types alone — e.g. for A → A, the only inhabitant is identity.
• Typed languages as proof assistants. Coq, Agda, Idris, Lean — all exploit the correspondence to turn programs into machine-checked proofs of the propositions their types denote.
• What "empty types" mean. A type with no inhabitants corresponds to a proposition with no proof — i.e. a false proposition. A function returning the empty type can't return at all; it must loop forever or throw.

Dependent types: propositions about values

Plain Curry-Howard maps types to propositional logic (no quantifiers over values). To express richer propositions like "this list is sorted" or "this index is in range," you need dependent types: types that depend on values.

sort : (xs : List Int) → SortedList xs

The return type mentions the input value. That's enough to encode all of predicate logic — and it's why dependently typed languages can express full mathematical theorems.

Clojure, being dynamically typed, doesn't have the machinery — but understanding Curry-Howard reframes what types are for: machine-checkable constraints on what programs are allowed to mean.

Try it in Clojure

You can see the logical reading of a function by writing both the program and the proposition side by side.

Each function above is, literally, a proof of the proposition its argument shape encodes. The dynamic typing means Clojure can't check the proof, but the structural correspondence is identical to Haskell or Coq.

Real-world: where Curry-Howard shows up shipped

The unifying point: whenever bugs in some software are unacceptable — kernels, crypto, compilers, money-handling contracts, math proofs of record — people reach for Curry-Howard's machinery.

Check yourself

Exercise

For each Clojure function below, name the logical proposition it proves:

(defn snd [a b] b)
(defn swap [[a b]] [b a])
(defn left-of [[tag val]] (when (= tag :left) val))

(Hint: write the type first, then translate to a logical statement.)