Reading Reflection 4
Due: Friday, May 15 at 5:00 PM | 50 points
AI is changing everything about how software gets built. What role does verification play when machines write the code?
Theme
Week 7 is called "The Future is Unwritten" because nobody knows how AI will reshape software development, but the three options below offer genuinely different visions. After six weeks of learning solver-aided reasoning, you have the technical background to evaluate these arguments on their merits. Your job is to take a position.
Some readings may be behind publisher paywalls. As a UW student, you have free access through the UW Libraries proxy. See the Resources page for setup instructions.
Options (pick one)
Option A: Keles 2025, "Verifiability is the Limit"
- Read it: alperenkeles.com
- Time: ~9 min
- Stance: Nuanced
The bottleneck for AI-assisted programming is not code generation but verification: the human ability to confirm that generated code matches intent. LLMs excel at UI code because verification is visual, but struggle with backend code where verification requires real reasoning. The skills you learned in CARS are the scarce resource.
Option B: Ronacher 2026, "The Final Bottleneck"
- Read it: lucumr.pocoo.org
- Time: ~8 min
- Stance: Nuanced
The creator of Flask argues that AI has inverted the development bottleneck: code generation is fast and cheap, but review, understanding, and accountability remain fundamentally human. Drawing on textile industrialization history, he insists that non-sentient machines cannot carry responsibility.
Option C: Kleppmann 2025, "AI Will Make Formal Verification Go Mainstream"
- Read it: martin.kleppmann.com
- Time: ~10 min
- Stance: Cheerleader
The author of Designing Data-Intensive Applications predicts that three forces will bring formal verification into the mainstream: AI reduces the cost of writing proofs, AI-generated code makes verification more important, and proof checkers provide reliable feedback for LLMs. He calls this "vericoding" in contrast to "vibecoding."
Reflection
After reading your chosen option, write a short reflection (~500 words) with three components:
-
Summary and main argument (~5 sentences). What is the author's central claim? What evidence or reasoning do they offer?
-
What resonated (~5 sentences). What connected to your own experience as a working engineer? What rang true?
-
What you questioned (~5 sentences). Where did you disagree, find gaps, or want to push back?
Submit via Gradescope by Friday at 5:00 PM. You may submit up to Monday at 8:00 AM with no penalty.
Grading
Each component is worth 10 points on a ternary scale:
| Score | Meaning |
|---|---|
| 3 | Surface-level: restates without engagement |
| 7 | Solid engagement with the ideas |
| 10 | Connects to your experience or course content |
Total: 30 points (individual) + 20 points (group discussion summary, completed in class the following Tuesday).
Enrichment
These are optional readings that go deeper into the themes raised by the three options above. You are not required to read any of them, but if one of the options left you wanting more, start here.
Congdon 2025, "The Coming Need for Formal Specification"
Written as a direct response to Kleppmann. A Databricks staff engineer agrees that AI will drive FM adoption but argues the bottleneck is specification writing, not proof generation. If Keles says verification is the limit and Kleppmann says proof generation will be automated, Congdon says the spec itself is where humans remain indispensable.
Thompson 2026, "Coding After Coders"
Vivid reporting from the world all three options describe. Over 70 developers at Google, Amazon, and Microsoft explain how their daily work has changed with AI tools. If Keles theorizes about the verification bottleneck and Ronacher argues for human accountability, Thompson shows you the people already living it.
Ye et al. 2025, "Verina: Benchmarking Verifiable Code Generation"
The hard data behind the predictions. The best current LLM achieves 72.6% on code generation but only 4.9% on proof generation. Verification is indeed the bottleneck, as Keles argues. If Kleppmann predicts AI will democratize FM, Verina shows how far there is to go.
Mugnier et al. 2025, "On the Impact of Formal Verification on Software Development"
What it actually feels like to use formal verification tools today. Interviews with 14 experienced Dafny users reveal "fearless optimization" as the biggest payoff and "soul crushing" proof brittleness as the biggest cost. Ground truth for evaluating whether Kleppmann's prediction of mainstream adoption is realistic.
Lamport 2006, "The Future of Computing: Logic or Biology"
A Turing Award winner framed the logic-vs-biology choice 20 years before Keles and Kleppmann. Should software be treated as a logical artifact amenable to proof, or as an emergent biological system? In the AI era, does the logical approach finally win, or does the biological metaphor describe what LLMs actually do?