Every Program Proves Something

In the mid-1930s Gerhard Gentzen, a German logician, wants to understand what a proof is. Not whether some theorem is true, but the anatomy of reasoning itself. He writes down a small set of rules for how you’re allowed to introduce and use “and,” “or,” and “implies.” He calls it natural deduction.

Around 1940 Alonzo Church, working on something else entirely, publishes a way to attach types to his λ-calculus, a tiny language made of nothing but functions. He wants to stop his system from eating itself with paradoxes. He isn’t thinking about Gentzen.

Decades later someone puts the two side by side and they are, in Philip Wadler’s words, essentially identical. Same rules. Same structure. Different handwriting. Wadler still calls this a mystery: why should two things built at the same time for unrelated purposes turn out to be one thing?

And then it happened again. And again. And again.

I’ve written here about Shannon, who noticed that communication and thermodynamics are secretly the same subject, and about von Neumann, who saw that a machine’s organization matters more than its parts. This is another one of those moments where two fields turn out to be the same field. But what gets me isn’t the famous slogan, “programs are proofs.” It’s that the connection runs both ways. Logicians discovered things that programmers later rebuilt without knowing. Programmers hacked together things that turned out to be pieces of logic nobody had written down yet. It’s a door, and people kept walking through it from both sides, for fifty years, without noticing it was a door.

First, the door itself. It’s small.

function swap<A, B>([a, b]: [A, B]): [B, A] {
  return [b, a];
}

Read the type as a sentence: if A and B, then B and A. A pair is “and.” Holding one means you have evidence for both halves. To return [B, A], you rearrange the evidence you were given. The function body is the proof.

The generics keep you honest. You know nothing about A, so you can’t make one up. The only A in your universe is the one someone handed you. That’s the logician’s rule exactly: no assuming the conclusion, only building it from what you’ve got.

function compose<A, B, C>(f: (a: A) => B, g: (b: B) => C): (a: A) => C {
  return (a) => g(f(a));
}

If A implies B, and B implies C, then A implies C. The syllogism. And calling f on an a is modus ponens, from “A implies B” and “A,” conclude “B.” Oldest inference rule there is.

This is the part I find funny as someone who builds multi-agent systems for a living. An agent calling a tool is the same move. The tool has a schema: give me a CustomerId, I’ll give you an Invoice. The agent produces a CustomerId, calls the tool, gets an Invoice. That’s modus ponens with a JSON schema standing in for the proposition. Every day, somewhere, large language models are doing logic from 350 BC and nobody calls it that.

The whole vocabulary lines up. “Or” is a tagged union, and the tag is the point: proving “A or B” means telling me which. “False” is a type with no values, never in TypeScript. “Not A” is a function from A into never. A type is a proposition. A value is a proof.

Haskell Curry noticed the first hint in 1934 and spelled it out with Robert Feys in 1958, but mostly treated it as a curiosity. His combinator K, which takes two arguments and returns the first, has the same shape as the axiom α ⊃ (β ⊃ α). Cute. Filed away.

William Howard didn’t file it away. His notes circulated privately in 1969, photocopies, no journal. He credited Curry for half the idea and W. Tait for the other half: Tait’s 1965 finding that simplifying proofs matches reducing λ-terms. That second half is the one that matters. When a logician removes a detour from a proof, a lemma used once that could be inlined, it’s the same operation as a CPU calling a function and substituting the argument. Proof simplification is program execution. They don’t just look alike. They move alike.

Still, one coincidence could be a pun. Here’s why it isn’t.

1969, logic side. Roger Hindley, a logician in Curry’s own field, is studying a question that sounds hopelessly abstract: given an expression, what’s the most general type it could have? He proves there’s always a best answer and shows how to compute it.

1970s, programming side. Robin Milner in Edinburgh is building ML, a language for writing a theorem prover. He’s tired of annotating types and wants the compiler to figure them out. He designs an inference algorithm.

Same system. Found independently. Hindley–Milner. Standard ML, Miranda and Haskell were built on it. Every time OCaml or Haskell figures out the type of a function you were too lazy to annotate, a logician’s theorem about combinators is running in there, and the guy who put it there didn’t need the logician to find it.

Around 1972, logic side. Jean-Yves Girard, a young French logician, is trying to understand second-order arithmetic, a very strong system where you can quantify over properties of numbers, not just numbers. He needs a calculus to interpret it. He builds System F.

1974, programming side. John Reynolds wants to understand polymorphism: how one function like swap can work at every type. He designs the polymorphic λ-calculus.

Same calculus. Different countries, different questions. Girard was interpreting second-order logic. Reynolds was doing functional programming. Neither needed the other.

This is where the two-way traffic stops being a metaphor.

Girard proved that every term in System F normalizes. For him, that was about proofs: every proof simplifies all the way down, which is how you show a logic holds together. Walk through the door and the same theorem says every System F program terminates. One proof, two results, one delivered to each field.

He also proved that every function on natural numbers that second-order logic can prove total can be written as a program in F. A map from logic into programs.

Reynolds, separately, proved an abstraction theorem that lets you read a logical fact off any program in F. A map from programs into logic.

Years later Wadler noticed that these two maps fit together. Embed programs into logic with Reynolds, project back with Girard, and you land exactly where you started. Two people working from opposite ends of a tunnel, never coordinating, and the tunnel meets in the middle.

I’ve built enough distributed systems to know how rarely two independently designed halves line up on the first try. Usually you get a week of integration hell and a meeting. These two lined up perfectly, across disciplines, without a spec.

Reynolds’s side of that tunnel gives you something weirdly practical. Wadler called it “theorems for free.”

function rev<A>(xs: A[]): A[]

Forget the name. Just the type. What can this function possibly do? It knows nothing about A. It can’t create one, compare two, or peek inside. All it can do is rearrange, drop or duplicate what it was handed.

So without reading the body, you already have a theorem. For any function g:

rev(xs.map(g))  ==  rev(xs).map(g)

Transform then shuffle equals shuffle then transform, because the shuffle is blind to the elements. You got a law from the type alone. No tests. No code review. (Assuming the function plays fair: no typeof tricks, no exceptions, no infinite loops. Cheating comes later.)

The type was the theorem the whole time. The compiler just never mentioned it.

Now my favorite one, because the door swings the other way.

1933, logic side. Gödel, and Gentzen in a slightly different form, find a way to translate classical logic, where everything is true or false, into constructive logic, where you have to actually build what you claim. The trick is to stick “not not” in front of things. Instead of proving A, prove that A can’t be refuted.

1972, programming side. Reynolds again, writing about continuation-passing style. Instead of returning a value, a function takes a callback, “the rest of the program,” and calls it with the result. Compiler writers use it internally. If you wrote Node.js before promises existed, you did it by hand and it was miserable.

They’re the same transformation.

type Not<A> = (a: A) => never;
type NotNot<A> = (k: Not<A>) => never;

function toNotNot<A>(a: A): NotNot<A> {
  return (k) => k(a);
}

As logic: “A implies not-not-A.” As code: “give me a callback and I’ll call it with this value.” That k is a continuation. A logician’s move from 1933 and the callback hell of 2012 are one function, read two ways. I think about this every time I see a pyramid of nested callbacks. It’s Gödel all the way down.

It gets better. Classically, “A or not A” is always true. Constructively you can’t write it. A generic function returning Or<A, Not<A>> doesn’t exist, because you’d have to pick a side knowing nothing about A. But you can write its double negation:

type Or<A, B> = { tag: "left"; value: A } | { tag: "right"; value: B };

function emNotRefutable<A>(): NotNot<Or<A, Not<A>>> {
  return (k) => k({ tag: "right", value: (a: A) => k({ tag: "left", value: a }) });
}

Read it as a con. The continuation k challenges you: excluded middle is false, prove me wrong. You say “not A.” If they ever come back holding a real A to catch you out, you call k again, from the top, and this time say “A,” using their own A against them. You win by rewinding and changing your answer.

Rewinding and changing your answer is exactly what a continuation lets a program do.

1990, and the door swings from the programmers’ side. Scheme had call/cc since the 70s. It captures “the rest of the computation” as a value you can jump back into. People used it for generators, coroutines, exceptions. It was a Lisp hacker’s tool. Nobody designed it as logic.

Timothy Griffin asked what type it should have. The answer was ((A → B) → A) → A, Peirce’s law, a classical principle that constructive logic refuses. He showed the correspondence everyone assumed was stuck in constructive logic extends to classical proofs once programs can reach the control context.

So a control-flow hack from the Lisp world turned out to be the exact missing piece between the logic of programs and the logic of textbook math. Classical logic is constructive logic plus a rewind button. The programmers built the button first. Logic found out later.

That one makes me happy for purely tribal reasons. I once wrote a distributed key/value store in Common Lisp for fun. Lisp people have been doing strange things with control flow for sixty years, and occasionally the strange thing turns out to be a theorem.

Wadler keeps a longer list of these pairs.

Modal logic, from C. I. Lewis around 1910, matches monads, the structure Haskell uses for state, exceptions and I/O, which Moggi brought into programming in 1987.

And Girard again, 1987: linear logic, where every assumption must be used exactly once, like a resource you can’t copy or throw away. It matches session types, from Kohei Honda in 1993, which describe protocols between communicating processes and let a compiler check that both sides follow them.

This one hits close to home. I spend a lot of time thinking about networks where messages sit in buffers for hours, as I wrote in A Network That Can Wait, and I built a delay-tolerant network simulator in Rust. The failure modes in that world are lost messages and duplicated messages. A logic where every fact is used exactly once, no more and no less, is the same thing as a type system for two machines that can’t drop or duplicate what they say to each other. Rust’s ownership model is a loose cousin of the same idea: a value you move is gone from where it was. Girard was working on proof theory. He ended up describing the thing I debug.

Wadler says Curry–Howard is a double-barrelled name that ensures the existence of other double-barrelled names. Curry–Howard, Hindley–Milner, Girard–Reynolds. Each one is a logician and a programmer who got to the same place without each other.

Now where the door jams. The jam is part of the story too.

function liar<T>(): T {
  throw new Error("trust me");
}

function forever<T>(): T {
  while (true) {}
}

Both compile in strict TypeScript. Both claim “for any T, a T,” which as logic reads “everything is true.” Once one of these exists, even never has an inhabitant and the logic is garbage.

Read Girard backwards. Good logic means every program terminates. Turn it around: a language where programs can loop forever can prove anything. Non-termination on one side and inconsistency on the other are the same disease, seen from opposite ends of the door.

This is where I have to confess where I live. Elixir is one of my main languages, and it sits on Erlang’s philosophy: let it crash. Processes die all the time and supervisors restart them. From the proof side, every crash is a proof of False. From the Erlang side, a crash is a Tuesday. Both views are right. They’re answering different questions. Proofs ask “can this ever go wrong?” Supervisors ask “when it goes wrong, what happens next?” Systems that run for years need the second question answered no matter how good your answer to the first one is.

Proof assistants pick the other side of the trade. Lean refuses this:

def loop2 (n : Nat) : False := loop2 n
-- error: fail to show termination for loop2

Its escape hatch, partial def, only works for types it can already see are inhabited, so you can’t sneak False through it either:

partial def loop (n : Nat) : False := loop n
-- error: ... could not prove that the type ∀ (n : Nat), False is nonempty

Nice try.

So in TypeScript, Rust, Go or Python with type hints, a well-typed program is a proof in a conditional sense: if it finishes and doesn’t cheat. That’s still worth a lot. It just isn’t a certificate.

Once you have a language where the door doesn’t jam, the two-way street becomes infrastructure.

In Lean, induction is recursion:

theorem zero_add' : (n : Nat) → 0 + n = n
  | 0     => rfl
  | n + 1 => congrArg (· + 1) (zero_add' n)

A recursive function and a proof by induction, in the same six lines. The termination checker that just rejected loop2 is what makes this induction valid instead of circular. Same check, two meanings.

“There exists” is a pair, witness plus evidence:

theorem exists_bigger (n : Nat) : ∃ m, m > n :=
  ⟨n + 1, Nat.lt_succ_self n⟩

The proof that a bigger number exists is the number.

This is how CompCert, a C compiler proven correct in Coq (now the Rocq Prover), became the only compiler where a Utah team’s random-program fuzzer found no wrong-code bugs in the middle-end after about six CPU-years of trying. The bugs it did find lived in parts that hadn’t been proven yet. Verification doesn’t remove bugs. It pushes them to the border of what you proved. MIT’s Fiat Cryptography generates elliptic-curve arithmetic together with its proof, and that code went into Google’s BoringSSL, which by the authors’ 2019 estimate handled about 90 percent of Chrome’s secure connections.

I used to work on fraud detection at around a billion checks a year. At that volume, a one-in-a-million edge case happens a thousand times. That’s the scale where “we tested it a lot” stops being a comforting sentence, and where a proof starts to look cheap.

And this is why I think the topic matters more in 2026 than it did in 1969.

A proof assistant has a small kernel that checks proof terms, and the kernel doesn’t care who wrote them. A grad student, a tactic, or a language model that’s wrong nine times out of ten all go through the same gate. If the term checks, it’s right.

I build systems where agents write code, call tools and make decisions, with humans approving the risky parts. The hardest problem in that world isn’t getting agents to do things. It’s knowing when to trust what they did. Curry–Howard offers a clean answer for one slice of it: let the unreliable writer be as creative as it wants, and put a small, boring, trustworthy checker at the end. It’s the same trick as Shannon’s error correction. You don’t make the channel perfect. You make the receiver able to tell.

The catch is the spec. The kernel checks that you proved your claim. It has no idea whether your claim is the one you meant. If the agent writes the spec too, you’re back to trusting the agent.

So why does this keep happening? Why do logicians and programmers keep building the same things without talking to each other?

Wadler’s answer is that it shows some aspects of programming are absolute, not arbitrary. When a French logician taming second-order arithmetic and an American computer scientist explaining generics write down the same system, that system probably isn’t a design choice. It was there before either of them.

My answer is more of an engineer’s hunch. Both of them were asking the same question: what can I build from what I’ve been given, without cheating? The logician asks it about truth. The programmer asks it about data. There seems to be only one answer, and it doesn’t care which door you came in through.

Next time the compiler accepts your code without complaint, remember that someone in the 1930s may have already written down what you just proved. They just didn’t know it would run.