The Truth of a Procedure
summary
A procedure gets judged by concrete rules: an interface prologue and epilogue, claim and usable assertions, and a game where the outside world names inputs and the procedure names outputs; failures incur precise penalties (delay of game, assertion failure, inconsistent naming, unmentioned aliasing). If the outside wins for some machine the procedure is merely possible; if the procedure wins for all machines it is necessary. Adding inlined claims or theorems can make a merely possible procedure provably necessary.
AI-written summary · about
chapters (13)
- 0:00Introduction
- 1:47Procedural logic
- 10:08Code
- 15:05Interface
- 21:51Function
- 26:28Basic Interface
- 27:24CanMultiply
- 29:52CanDecrement
- 30:41Epilogue
- 36:28Dense Linear Orderings
- 38:48Ensembles
- 50:02Theorems
- 53:18Game of Proof
related talks
01h 30mValue in a Procedural World
57mMy favorite verbose programming technique
29mProcedural Macros vs Sliced Bread
01h 27mDeclarative thinking, declarative practice
42mWhat If We Pretended Unsafe Code Was Nice, And Then It Was?
57mBetter Code: Exploring Validity in C++
57mBack to Basics: The Abstract Machine
07mAssertions of Competence