Reading Reflection 1
Due: Friday, April 3 at 5:00 PM | 50 points
This quarter opens with a provocation: what if formal methods are not worth it? Before we start writing solver-aided code, we read the critics.
Theme
Week 1 is called "Engage the Skeptics" because we start by taking the critics seriously. Each of the three options below questions whether formal methods deliver on their promises. Your job is to read one, sit with the argument, and write honestly about what you think.
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: Gabriel 1991, "The Rise of Worse is Better"
- Read it: dreamsongs.com
- Time: ~15 min
- Stance: Critic (design philosophy)
The classic argument that simpler, imperfect systems beat correct, complex ones through viral adoption. At 3 pages, the shortest reading in the library and the one most likely to start an argument.
Option B: Dodds 2025, "What Works (and Doesn't) Selling Formal Methods"
- Read it: galois.com
- Time: ~15 min
- Stance: Critic (economic)
A Galois principal researcher, whose company built verified cryptographic tools for AWS, admits that most formal methods projects do not pencil out economically.
Option C: Hoare 1996, "How Did Software Get So Reliable Without Proof?"
- Read it: doi.org
- Time: ~40 min
- Stance: Nuanced (insider confession)
The inventor of Hoare Logic honestly asks why his own research program has not transformed practice. A Turing Award winner questioning his life's work.
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.
DeMillo, Lipton, Perlis 1979, "Social Processes and Proofs of Theorems and Programs"
The philosophical foundation for the skeptic's case. DeMillo argues that formal proofs of programs cannot participate in the social processes that make mathematical proofs credible. If you read Dodds and want deeper foundations for the economic argument, start here. If you read Gabriel, this is the attack from above: philosophy against correctness. If you read Hoare, this is the critique he was implicitly responding to.
Wayne 2019, "Why Don't People Use Formal Methods?"
A comprehensive landscape of why adoption has stalled. Wayne's observation that 90-99% correct is dramatically cheaper than 100% is the quantified version of Gabriel's "worse is better" instinct. His code-verification vs. design-verification distinction deepens the economic argument Dodds makes.
Fetzer 1988, "Program Verification: The Very Idea"
The ontological objection: programs are physical, not abstract, so formal verification cannot work in principle. A deeper level than Dodds ("FM doesn't pencil out") or Gabriel ("worse wins"). If you find the economic arguments unsatisfying, try this philosophical one.
Majors 2019, "I Test in Prod"
The pragmatic alternative to formal methods: invest in observability, production resilience, and deploy tooling instead of pre-production proofs. If Hoare asks how software got reliable without proof, Majors has an answer: monitoring, error budgets, and shipping fast.
Thompson 1984, "Reflections on Trusting Trust"
Ken Thompson's Turing Award lecture showing a class of problem where no amount of verification helps: if the compiler is compromised, source-level proofs are meaningless. A fundamental limit on what any formal method can guarantee.
Lamport 2015, "Who Builds a House Without Drawing Blueprints?"
The affirmative counterweight to every skeptic on this page. A Turing Award winner argues that specification-first engineering is a professional responsibility, not an unaffordable luxury. If you found the critics convincing, test that conviction here.