Principia Mathematica
The Foundations of Arithmetic in C++
The C++ integral arithmetic operations present a challenge in formal interface design. Their preconditions are nontrivial, their postconditions are exacting, and they are deeply interconnected by mathematical theorems. I will address this challenge, presenting interfaces, theorems, and proofs in a lightly extended C++.
This talk takes its title from Bertrand Russell’s and Alfred North Whitehead’s logicist tour de force, Principia Mathematica. It echoes that work in developing arithmetic from first principles, but starts from procedural first principles: stability of objects, substitutability of values, and repeatability of operations.
In sum, this talk is one part formal interface design, one part tour of C++ integral arithmetic, one part foundations of arithmetic, and one part writing mathematical proofs procedurally.
Lisa Lippincott
Lisa Lippincott designed the software architectures of Tanium and BigFix, two systems for managing large fleets of computers. She's currently chair of the numerics study group of the C++ standardization committee. In her spare time, she studies mathematical logic, and wants to make computer-checked proofs of correctness a routine part of programming.