KEYNOTE: The Shape of a Program
summary
Programs model as a bitopological manifold with two topologies — one for entrances and one for exits — so time becomes directional adjacency instead of symmetric edges. Assertions act as local, repeatable experiments that bend topology so tests leave no meaningful effect. Capabilities like D allocatable, readable, writable form tunnels through time that enforce resource conservation (preventing leaks and double frees) and carry values; interfaces appear as prologue/epilogue pairs that are nestable, letting proofs be local while others remain positive assumptions. The talk uses conceptual “fantasy C++” extensions rather than a released tool.
AI-written summary · about
chapters (15)
- 0:00Introduction
- 2:20Locality
- 5:34Topology
- 10:15Directional Space
- 14:37Connection
- 22:59Preconditions
- 28:41Two kinds of assertions
- 30:50How to use maps
- 33:48Interface notation
- 36:19Interface repeatability
- 37:48Implementation gap
- 44:03Heap
- 46:31Copy Construction
- 48:45If Statement
- 54:53Dual Assignment
related talks
01h 09mPlenary: Neighborhoods Banding Together: Reasoning Globally about Programs
51mKeynote: There Is No Silver Bullet to Solve All C++ Software Problems
52mThink Abstractly, Work Concretely
01h 03mKeynote: Abstraction Patterns
01h 23mMidnote: Why Cpp Loops End
01h 02mProcedural Programming: It Never Went Away
43mThursday Keynote -- What Programming is Really About
22mA Categorical Basis for Robust Program Analysis