New preprint: Programming Really Is Simple Mathematics

Bertrand Meyer and Reto Weber: Meaning as ProgramsProgramming Really Is Simple Mathematics, February 2025 preprint available here and also on arXiv.

Theories of programming can be quite complicated; the presentation here is a return to essentials, defining programming and associated concepts (programming languages, programming methodology) entirely from elementary set-theoretical concepts.

Unlike much of the work in formal methods, which forces the reader to go through many axioms and definitions for little benefit, this approach, called PRISM (Programming Really Is Simple Mathematics) is axiom-poor and theorem-rich. In fact it has zero axioms: it simply relies on the well-known properties of set theory to define programming on the basis of one set and one relation. Then it builds up programming mechanisms as simple objects (sets, relations, functions, composition…) and proves theorem after theorem highlighting their properties.

This approach was started in a 2015 article (cited in the new publication) but now, thanks to Reto Weber (a PhD student at CIT), it has the benefit of extensive proofs all checked by Isabelle/HOL; the corresponding files are publicly available.

The article covers the general framework, including the mathematical background (basically high-school-level elementary set theory with a few convenient notations for things like domain of a relation), basic constructs, control structures (sequence, conditional, loops of various kinds), refinement (treated as “subset”), specification vs. implementation, contracts, invariants, and concurrency.

The ambition is to reconstruct all of programming in this spirit.

Here is the more formal abstract from the paper itself:

A re-construction of the fundamentals of programming as a small mathematical theory
(“PRISM”) based on elementary set theory. Highlights:

  • Zero axioms. No properties are assumed, all are proved (from standard set theory).
  • A single concept covers specifications and programs.
  • Its definition only involves one relation and one set.
  • Everything proceeds from three operations: choice, composition and restriction.
  • These techniques suffice to derive the axioms of classic papers on the “laws of pro-
    gramming” as consequences and prove them mechanically.
  • The ordinary subset operator suffices to define both the notion of program correctness
    and the concepts of specialization and refinement.
  • From this basis, the theory deduces dozens of theorems characterizing important
    properties of programs and programming.
  • All these theorems have been mechanically verified (using Isabelle/HOL); the proofs
    are available in a public repository.

Reminder: my full annotated publication list is here.

VN:F [1.9.10_1130]
Rating: 0.0/10 (0 votes cast)
VN:F [1.9.10_1130]
Rating: 0 (from 0 votes)
Be Sociable, Share!

Leave a Reply

You must be logged in to post a comment.