The Unexpected Bridge Between Logic and Programming
The Curry-Howard correspondence, discovered independently by Haskell Curry in 1934 and William Howard in 1969, reveals that types are propositions and programs are proofs. Writing a program that type-checks is equivalent to constructing a mathematical proof. This is not a metaphor — it is a precise structural isomorphism between two independently developed formal systems.
Types as Specifications
A type signature f : Int to Bool is a claim: given an integer, this function produces a boolean. Type checking verifies this claim mechanically. But simple types are shallow specifications — they say nothing about whether the integer must be positive, or
The Simply-Typed Lambda Calculus
Adding types to the lambda calculus gives the simply-typed lambda calculus (STLC). Every term has a type, and the type system rejects terms that would get stuck — applying a number as a function, for instance. The correspondence: the type A to B correspon
Dependent Types
In dependent type theory, types can depend on values. The type Vector n a is the type of lists of length exactly n containing elements of type a. The length is part of the type. A function append : Vector m a to Vector n a to Vector (m+n) a encodes the fa
Proof Assistants and Formal Verification
Coq and Agda are proof assistants based on dependent type theory. Writing a program in Coq means constructing a proof that the program meets its specification. The seL4 microkernel — used in safety-critical embedded systems — was verified in Coq: a machin
"The seL4 verification does not mean the system is perfect. It means every security property stated in the specification is guaranteed by mathematical proof. The specification itself is a human product and may be wrong. Proof moves the uncertainty from the
"KaiRenner24th of March 2026
Homotopy Type Theory
Homotopy Type Theory (HoTT) is a recent unification of type theory with algebraic topology. Types are interpreted as topological spaces, and proofs of equality are interpreted as paths between points. This provides a new foundation for mathematics in whic
Go Deeper: Type Theory as a Foundation for Mathematics
Type theory is one proposed foundation for all of mathematics — an alternative to set theory. Classical mathematics is usually founded on set theory, and set theory has its own surprising paradoxes and fundamental limitations that took decades to resolve. Those limitations illuminate why foundations matter.
