The Proof Already Contains the Program: One rewrite theory from every logic to running code

Abstract

Trust in a proof is supposed to rest on a kernel small enough to read by hand. The formal-methods ecosystem has instead grown a dozen large, mutually opaque kernels—one per proof assistant—and now machine learning floods all of them with proofs and programs no human can eyeball. We report a working demonstration that the escape from this predicament is a single, small, well-understood mathematical object: the λΠ-calculus modulo rewriting, a typed lambda calculus with user computation rules into which functional type theories are known to embed. We realize eight source systems—Coq/CIC, Lean 4, HOL Light, Isabelle/Pure, Agda, Metamath, GHC's System FC, and Rust's typed MIR—as exact, faithfully translated images inside one such checker, so that eight trust roots collapse to one. Then we show the same object runs in reverse: because a constructive proof already contains its program (the Brouwer–Heyting–Kolmogorov reading of Curry–Howard), the checked content of each image extracts, through one back-end, to a whole-program Rust artifact that a compiler builds and runs against a certified differential—for all eight languages. One small kernel receives every logic and emits its program. The consequence is a concrete first step toward software engineering done mathematics-first: you audit a tiny shared checker rather than trusting the author, human or machine, and the verified proof is the deployable artifact. A fresh finite logical-entropy estimator now tests that extraction thesis on an object not used to build the original eight-door demonstration: its exact ensemble law is proved in Lean, its Rust realization returns the same unreduced rational pair, and applicable structural mutations are killed. A successor program, reported in §6, has since walked this paper's own roadmap: export depth past scalars, an independent dual-metal differential through the Boundary reducer, an exactly enumerated residual trust base, and a proved composition theorem making source-kernel-to-bare-metal a single certified arrow. Published by The Institute for Applied Ontological Mathematics.