LT: Proof Driven Development
summary
An experiment uses Livebook notebooks as fixed, executable invariants and a CI checkpoint to guide agents to implement orbital mechanics; six notebooks cover separate properties including mechanics, generalization and complexity. An early run with Claude Haiku 45 from memory crashes the notebook, plain markdown prompts produce accidental but unverified results, while livebooks detect a sign flip that causes 37 km drift per orbit, flag a complexity regression versus linear, and auto-fix the code (quadratic accumulation) in one turn.
AI-written summary · about
related talks
18mCoding Evals: From Code Snippets to Codebases
23mBeyond Tests What to Verify in AI Generated Code
08mExample-driven development: bridging tests and documentation
29mTDD shouldn't be TDDious
01h 12mDistributed systems showdown — TLA + vs real code
56mMy Journey to the Dark Side: Under-Approximation, Incorrectness, Proof
48mDomain Invariants & Property-Based Testing for the Masses
01h 30mNo (lab) jacket required