Mirqāt The Ascent of Logic

A thread · guided journey

Proof Becomes Computation

The slow discovery that a proof and a program are the same thing, from Gentzen’s rules to the proof assistants of today.

  1. 01

    Gentzen’s Insight

    Cut-Elimination (Hauptsatz)

    Gentzen shows a proof has structure: cut-elimination turns any proof into a direct, detour-free one. A proof, it seems, can be *run*: simplified, step by step.

  2. 02

    Church & Turing

    Undecidability of the Halting Problem

    Independently, Church’s λ-calculus and Turing’s machine pin down exactly what “computable” means, and show that some questions no computation can answer.

  3. 03

    The Identity: Curry–Howard

    Curry–Howard Correspondence

    The revelation: propositions *are* types, and proofs *are* programs. To prove a theorem is to write a program of a certain type. Logic and computation are one structure.

  4. 04

    Martin-Löf’s Foundation

    Per Martin-Löf Intuitionistic Type Theory 1984

    Martin-Löf builds a whole foundation on this: dependent type theory, where mathematics is done by constructing objects, and a proof is a program you can check.

  5. 05

    Into the Machine

    Computational Logic

    Today the correspondence is concrete: Lean, Coq, and Agda are languages in which mathematicians write proofs that the computer checks, and sometimes helps discover.

← All threads