Toward Programming Languages for Reasoning -- Humans, Symbolic Systems, and AI ...
summary
Argues that programming should be a substrate for reasoning and presents the Bosque core plus a developer-friendly surface that eliminates loops, enforces immutability, and gives fully determined semantics so analyzers never face undefined behavior. Prototypes compile directly to SMT (Z3), use a decidable fragment for collections, find concrete counterexamples in ~0.5s per unit test, and search small models (≤5 elements); experiments scale to thousands of lines and improve LLM-generated fixes via embedded examples and ensures.
AI-written summary · about
chapters (14)
- 0:00Programming language purpose
- 1:26Programming languages for reasoning
- 2:52Automated code reasoning challenges
- 6:04Poor reasoning support costs
- 7:05Reasoning-optimized language vision
- 8:07Core IR design principles
- 9:33Core IR vs human syntax
- 10:58Bosy language features
- 15:14Small model verifier demo
- 18:27AI coding with explicit intent
- 20:15Requirement gathering with defer
- 22:25Development substrates
- 24:30Future opportunities
- 25:16Q&A
related talks
15mCurrent Practices for Building LLM-Powered Reasoning Tools Are Ad Hoc—and We Can Do Better
41m"Do What I Mean": The History of AI and Program Synthesis
34mProgramming Languages for AI Programing Agents
17mHow to Program like a Five Year Old in Haskell
30mOpen Challenges for Programming Agents
01h 04mInvited Talk: Finding Good Programs by Avoiding Bad Ones
46mProlog: A Mature but Underrated Language for Symbolic AI
36mRethinking legacy modernisation with automated reasoning and comprehension models