Principia Mathematica - The Foundations of Arithmetic in C++
summary
This work gives concrete, machine-checkable interfaces and proofs for C++ integer arithmetic: extended function syntax with a prologue/epilogue, formal preconditions for undefined behavior, and implementations of stability, substitutability, repeatability. It defines integer kinds, convert modular/convert narrowing and widening types, builds an add-with-carry reference and an axiom to avoid blown-up interfaces, and encodes proofs (e.g., commutativity of addition) as executable claims. Code and slides live on the CppCon2022 GitHub and the examples compile and check.
AI-written summary · about
chapters (22)
- 0:00Start
- 5:37Function Interface
- 8:17Repeatability
- 8:46Stability
- 10:57Substitutability
- 16:52Interface for Assignment between Two Integers
- 18:45Integer Types
- 19:05Integral Types
- 26:04Convert Modular
- 29:18Interface
- 33:18Integral Promotion
- 40:01Arithmetic Conversions
- 40:57Integer Kinds
- 44:12Convert Modular to an Unsigned Type
- 45:06Uniform Arithmetic Conversions
- 50:24Shift Operations
- 57:25Widening Types
- 1:00:02Conversions to and from the Widening Types
- 1:00:32Break the Recursion
- 1:09:17The Axiom of Reducibility
- 1:11:59Split Bits and Join Bits
- 1:24:15One Bit Cases
related talks
55mClean Integral Code
57mBack to Basics: The Abstract Machine
01h 02mAn Overview of C++11/14, Part I
01h 02mEmbedded Friendly C++: Features That Make a Difference
01h 06mBack to Basics: Functions in C++
37mA (Not So Gentle) Introduction To Systems Programming In ATS
44mThis is why we can('t) have nice things
01h 49mKeynote: What C++ is and what it will become