The Truth of a Procedure
summary
Programs model procedures as formal sentences and truth is decided by a two-player game where the implementation (center court) and interfaces (prologues/epilogues) are played in nested turns. Claims like usable and substitutable claims, aliasing and branch directions control who loses; a delay-of-game penalty prevents infinite stalling. The factorial example fails until a theorem linking “>0” to “decrementable” is added. Allowing insertion of finite theorems yields a proof game whose winner corresponds to necessity (universal truth) or existence of a counterexample.
AI-written summary · about
chapters (10)
- 0:00The problem with formal proofs
- 2:54Defining procedural logic
- 5:11The game of truth
- 9:20Code as a playing field
- 13:57Factorial example walkthrough
- 25:08Winning strategies
- 30:17Necessary vs possible truths
- 34:02Game of proof
- 44:28Godel's completeness theorem
- 50:37Q&A and conclusion
related talks
18mIntroduction and Elimination, Left and Right
18mDeferring the Details and Deriving Programs
41mLiving inside a Theorem Proving Universe
01h 34mFormal Logic Undressed
18mEquivalence and Similarity Refutation for Probabilistic Programs
30mRelatively Complete Verification of Probabilistic Programs
34mA Taste of Prolog
33mA Historical Perspective on Program Transformation and Recent Developments (Invi...