Coding Agents: New opportunities for formal methods?
summary
Panel shows coding agents accelerate theorem proving but create new verification and tooling work. Agents generate huge artifacts (one project yields a 18,000-line Lean proof), agents then refactor them to half size and in other cases produce three- to four-fold smaller proofs. Workflows use Lean, SMT solvers, Rust borrow checking, Ergo/ASP and Codex; one agent even spawned a Lean subprocess to inspect proof state. Results speed proof creation and pattern discovery but introduce maintenance, audit and specification gaps that still fail without expert oversight.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 2:53Formal methods golden age?
- 11:51Programming languages today
- 17:53Debugging coding agents
- 24:54Future of programming languages
- 31:27Refinement types & theorem proving
- 36:04Type systems for coding agents
- 41:28Coding agents discovering proofs
- 47:05Human-computer interfaces
- 52:25Teaching programming now
- 1:05:47Advice for students
- 1:15:00Closing
related talks
16mBeyond the IDE: The Future of Developing Software With Agents
38mCoding Agents & Language Evolution: Navigating Uncharted Waters
40mBuilding Effective AI Agents Simple, Composable Patterns
30mHow AI Agents Will Change the Future of Programming
27mAgentic Coding with Discipline & Skill: Practical Techniques and Tips
29mPairing with the machine: How AI Agents are rewriting the rules of software development
24mRecursive Coding Agents
45mPanel Discussion on AI for Code Generation