Programming Really Is Simple Mathematics

[Submitted on 24 Feb 2025 (v1), last revised 27 Feb 2025 (this version, v3)]

View PDF

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]