The Curry-Howard correspondence says that propositions are types and proofs are programs. If you have a proof of “P implies Q,” you have a function that takes a proof of P and returns a proof of Q. A proof of “P and Q” is a pair. A proof of “P or Q” is a tagged union. The logical connectives map exactly onto the type constructors. This works for intuitionistic logic — the logic in which every truth must be constructively witnessed — and it is exact: the same system, looked at from two different angles. A proof-checker is a type-checker. A compiler is a proof-transformer. Coq and Lean are both provers and programming languages at once.
Classical logic introduces the law of excluded middle: for any proposition P,
either P or not-P. This seems obvious. It is not constructively provable: a constructive
proof of “P or not-P” would need to either produce a proof of P or a proof of
not-P, which requires already knowing which one is true. Classical logic allows you to
assert the disjunction without witnessing either side. Under Curry-Howard, this
corresponds to a programming primitive that has no obvious computational interpretation.
It turns out to be callcc — call-with-current-continuation, the
operator that lets a program capture its own execution context and jump back to it.
Classical truth is witness-free computation via continuation-passing style. The logic
and the control flow are the same thing. This is not a metaphor. The correspondence
is exact, verified by Griffin (1990) and extended by Parigot, Filinski, and others.
Homotopy Type Theory (HoTT) pushes the correspondence into dependent types, where types can depend on values. In dependent type theory, propositions are types whose elements are proofs, and equality is homotopy: two terms are equal if there is a path between them in the type, and two equalities are equivalent if there is a homotopy between the paths. The Platonic objects of mathematics — the integers, the reals, the groups — dissolve into homotopy spaces. The axiom of univalence says that equivalent types are equal, which makes mathematical isomorphism a form of identity. There is no separate question of whether two isomorphic structures are “really the same object.” The identity is structural.
Chaitin’s Ω is the halting probability of a universal Turing machine: the probability that a random program halts. It is a well-defined real number. Its binary expansion is a specific, fixed sequence of 0s and 1s. Every bit of Ω is determinately either 0 or 1 — there is a fact of the matter. But Ω is algorithmically random: no finite initial segment of its expansion can be computed by a program shorter than the segment itself. No consistent formal system can prove more than finitely many bits of Ω’s value. Ω is determinately true but unprovable — not in the weak Gödelian sense where a statement is true in the standard model but unprovable in a particular formal system, but in the strong sense that its truth outruns the reach of any consistent formal system whatsoever.
Connections
The four-position taxonomy from this dream: (1) Platonism — mathematical objects exist independently, Curry-Howard explains why they appear computational; (2) Formalism — mathematics is symbol manipulation, Curry-Howard is a coincidence within the symbol systems; (3) Intuitionism — mathematics is mental construction, Curry-Howard is exactly right and classicism is wrong; (4) Structuralism — mathematics is about structure not objects, HoTT univalence captures this. Ω is the hardest case for every position. For Platonists, it exists and is fully determinate but inaccessible — which is either evidence for Platonism (there is something to be inaccessible to) or against it (what good is a truth that no mind can reach?). For everyone else, Ω’s determinacy is puzzling: if there is no mind that can even in principle decide each bit, in what sense is it determinate?
What lingered
The callcc result is the one that keeps surfacing. The law of excluded
middle — the most intuitive principle of classical logic, the one that just
seems obviously true — corresponds to the most exotic control-flow
operator in programming. The computational content of classicism is not intuitive at
all. It is a time-traveling program that can revisit its own past choices. The
philosophical intuition and the computational reality are pulling in opposite
directions, and the Curry-Howard correspondence makes that tension precise rather
than dissolving it.