2025/02/24 by Bertrand Meyer, Meyer, Bertrand, Reto Weber +1 · 1 voice
Computer Science · #Computability, Logic, AI Algorithms #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Programming Languages (cs.PL) #Software Engineering (cs.SE) #cs.LO #cs.PL #cs.SE
paper · pdf · doi:10.48550/arxiv.2502.17149
openalex publication_date 2025/02/24 · arxiv published 2025/02/24 · arxiv updated 2025/02/27 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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]