Programming Really Is Simple Mathematics
Bertrand Meyer, Reto Weber
TL;DR
Programming Really Is Simple Mathematics reframes programming as a purely mathematical theory (PRISM) grounded in elementary set theory, dispensing with axioms and treating programs as mathematical objects defined by a postcondition and a precondition. It derives program constructs from three operators—restriction, choice ($\cup$), and composition ($;$)—and formalizes concepts such as feasibility, rounding, and refinement within this axiom-free framework, with all results mechanically verified in Isabelle/HOL. The paper argues that many traditional programming semantics and laws become theorems within this theory, offering a simplification of the foundations of programming and enabling rigorous, machine-checked proofs of key properties. It further connects refinement, specialization, and implementation to basic operations, and introduces conditional instructions as a natural extension of restriction and choice, thus providing a coherent, executable mathematical account of core programming concepts and their interrelations.
Abstract
A re-construction of the fundamentals of programming as a small mathematical theory (PRISM) based on elementary set theory. Highlights: $\bullet$ Zero axioms. No properties are assumed, all are proved (from standard set theory). $\bullet$ A single concept covers specifications and programs. $\bullet$ Its definition only involves one relation and one set. $\bullet$ Everything proceeds from three operations: choice, composition and restriction. $\bullet$ These techniques suffice to derive the axioms of classic papers on the "laws of programming" as consequences and prove them mechanically. $\bullet$ The ordinary subset operator suffices to define both the notion of program correctness and the concepts of specialization and refinement. $\bullet$ From this basis, the theory deduces dozens of theorems characterizing important properties of programs and programming. $\bullet$ All these theorems have been mechanically verified (using Isabelle/HOL); the proofs are available in a public repository. This paper is a considerable extension and rewrite of an earlier contribution [arXiv:1507.00723]