Programming Really Is Simple Mathematics

TL;DR

This paper reconstructs the fundamentals of programming as a simple mathematical theory based on set theory, deriving key properties and laws mechanically verified using Isabelle/HOL.

Contribution

It introduces PRISM, a minimal set-theoretic framework for programming, deriving laws and properties from only three operations and a single relation, with proofs mechanized.

Findings

Derivation of classical programming laws from minimal axioms

Mechanized verification of theorems using Isabelle/HOL

Unified theory covering specifications, programs, and correctness

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]