Midnote: Why Cpp Loops End
summary
Introduces a concrete scheme that embeds termination reasons in lightly extended C++ interfaces so an algorithm can check them, focusing on stability, substitutability, repetition as the machine-observable facts. Demonstrates machine-checkable proofs: why branching on literal true/false ends, how a primitive not_equal interface avoids recursion, when a static_assert short-circuits numeric cases, and a reusable counting theorem built with widening integers and reference axioms that mechanically proves typical count-to loops terminate.
AI-written summary · about
chapters (11)
- 0:00Why loops end
- 1:26Cosmological loop termination
- 5:45Robot-understandable loop reason
- 9:19Simple loops and proofs
- 22:40Counting to twelve with interfaces
- 31:21Universal loop termination
- 40:52Local events and variants
- 55:15Breaking down integers
- 1:01:14Counting theorem implementation
- 1:17:19Practical loop termination
- 1:20:31Future loop requirements
related talks
01h 01mSome Programming Myths Revisited
01h 05m“Contract Programming in C++(20) (part 2 of 2)”
54mReasoning about Progress of Concurrent Objects
01h 01mEasy to Use, Hard to Misuse: Declarative Style in C++
32mCute C++ Tricks, Part 2 of N: More code you should learn from and never write
01h 03m“Contract Programming in C++(20) (part 1 of 2)”
51mC++ ...Easy, Elegant, Powerful!
24mProving False in Object Oriented Verification Programs by Exploiting Non-Termination