Reading Reflection 1

Due: Friday, April 3 at 5:00 PM | 50 points

We start with doubt. Three people you might expect to champion formal methods raise questions instead. A company that sells them, a design philosopher who cares about correctness, and the inventor of Hoare Logic each question whether the promises hold up.

Theme

The theme for this reflection is "The Case Against?" Not all of these authors are skeptics. Two of the three have spent their careers building and selling formal methods. But each one, from a different vantage point, raises a genuine question about whether the promises hold up. Your job is to read one, take the argument seriously, 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: Dodds 2025, What Works (and Doesn't) Selling Formal Methods

Dodds works at Galois, a company that sells formal methods to industry. He loves FM. And he is here to tell you that most potential FM projects do not pencil out. The cost-benefit curve is bad: you spend a lot of money writing definitions and proving lemmas before you see any benefit. Clients do not care about correctness as such, because they have priced in bugs and their current processes work well enough. Cheap techniques like testing and code review are effective and much cheaper. This is not a theoretical argument against FM. It is a report from someone who has been on the sales calls and watched the conversations end.

Option B: Gabriel 1991, The Rise of Worse is Better

Gabriel sorts designers into two camps. MIT wants the right thing: correct, consistent, complete. New Jersey wants the simple thing to implement, even if the interface is ugly and the corner cases are broken. Unix and C spread because they were easy to port to weak hardware and shipped 50% of the right thing early, while Lisp was still being designed. Gabriel calls them "the ultimate computer viruses." Three pages, the shortest reading in the library, and the one most likely to start an argument about whether prioritizing correctness is a losing competitive strategy.

Option C: Hoare 1996, How Did Software Get So Reliable Without Proof?

Hoare created the logic that underlies program verification, then asked why the catastrophe it was meant to prevent never arrived. Mackenzie counted about ten software-caused deaths in twenty years, and the telecoms and aviation systems nobody proved correct were running on tens of millions of reliable lines. His answer is that design review, testing, debugging, and defensive over-engineering carried the weight, while formal methods research shaped practice indirectly through structured programming, type systems, and assertions. A Turing Award winner explaining how the thing his career was built on shaped practice without anyone using it directly.

Enrichment

These are optional readings that go deeper into the themes raised by the three options above. You do not need to read any of them, but if one of the options left you wanting more, start here.

Brooks 1986, No Silver Bullet

If you read Dodds and wanted a structural explanation for why FM struggles economically, Brooks provides the framework. He splits software difficulty into essence (the inherent complexity of what the system does) and accidents (the friction of saying so in code). Verification, Brooks argues, can only confirm that code meets a specification, but arriving at the specification is where most of the real work happens, and no tool touches that. Dodds's clients are buying a proof and getting a bill for the essential work that proof cannot do.

Thompson 1984, Reflections on Trusting Trust

Pairs especially well with Hoare. Hoare asks why software got reliable without proof; Thompson shows a class of attack where the proof would not help anyway. A compiler can be modified to insert a backdoor into the login command and re-insert the backdoor machinery into every future compiler it compiles. Once installed in binary, the source can be scrubbed clean and the attack persists. Three pages from the designer of Unix. One devastating argument.

If you read Gabriel and wanted a philosophical foundation for the skeptic's case, this is it. Mathematical proofs earn trust by being read, explained at blackboards, generalized, and reused as lemmas in other proofs. DeMillo, Lipton, and Perlis argue that program verifications can do none of that: they are too long, too mechanical, and too tied to one specific program. Even a perfect automatic verifier, they argue, would just hand you a result you cannot read, internalize, or apply anywhere else. Fifty years of formal methods work have been, in part, an extended reply.

Naur 1985, Programming as Theory Building

If the other readings on this page left you wondering whether formal methods are aiming at the wrong target entirely, Naur makes that case. The essential product of programming, he argues, is a theory (in Ryle's sense) held in the heads of the programmers who built it: how the world maps onto program execution, why each piece of the program is what it is, and how to respond to a modification request. Documents, specifications, and proofs are secondary artifacts. When the team holding the theory dissolves, the program dies, and reviving it from documentation alone is usually more expensive than starting over. If Naur is right, a verified specification is still outside the thing that matters.

See Reading Reflections for submission format and grading.