CSE 331 Reading 2

Due Friday, October 16 at 11:59pm (late policy).

Our motto for this course is: Your job is to deliver code that you know works. Knowing takes work: saying exactly what a method must do, testing it, and reasoning about whether it does that. Is that work the job itself, or a tax on the job?

The three articles below take three positions. Gabriel says that software which is simple to build spreads and wins, even when it is not quite right, and that getting it right can come later. Lamport says a program is a mathematical object, so every programmer should be able to say what their program means and whether they could prove it means that. Dijkstra says the formal care is the whole point, and that wanting to tell a computer what to do in plain English is a mistake.

Your task: Choose one article, read it, and write a reflection. See the readings page for information on what you need to submit and how reflections are graded. When you are done, submit on Gradescope as described in the "Submit" section below.

Each title below is a link to the original. If for any reason a link does not work, you can also use the "cached" links, which point to copies stored on UW servers: a PDF of each article and, for some, an HTML version that is easier to read with a screen reader or on a phone. (Cached links require UW NetID login).

Articles

Gabriel 1991, The Rise of Worse is Better

Gabriel helped design Common Lisp, a language built to be "the right thing". This is a short section of a longer essay about Lisp. It describes two ways to design software. One puts a simple interface ahead of a simple implementation. The other puts the implementation first, and lets the people who use it do the extra work. Gabriel admits to making the second one sound bad on purpose, then argues that it wins anyway: Unix and C gave people half of what they wanted, were easy to port, and spread like a virus. The advice is to ship half of "the right thing" first and improve it once people depend on it, with one condition: the half has to be basically right. The story in the middle is about a system call that fails and makes the caller check and retry, the same choice we face when handling errors. This was written in 1991, so its prediction about 1995 is a bet, not a report. About 10 minutes to read (cached: PDF, HTML).

Lamport 2003, The Future of Computing: Logic or Biology

Lamport gave this talk in 2003, so its "twenty years ago" is the early 1980s. Its examples are the email of that time and a mail program you may never have used. Floyd and Hoare showed how to prove a program correct, and Lamport grants that almost nobody does. What they gave us, the talk says, is a way of thinking: a program is a mathematical object, so you can ask what it means and whether you could prove it does that. Lamport does not ask you to write the proof, only to ask whether you could. When programs get too complex to understand, people fall back on superstition, avoiding whatever crashed last time. Treating software as a living thing that evolves means giving up on understanding it. Near its end, the talk blames universities for teaching a second programming course as if the first one's rigor never happened. That is a claim about courses like this one. About 20 minutes to read (cached: PDF, HTML).

Dijkstra 1978, On the foolishness of "natural language programming"

Dijkstra wrote this in 1978, long before any machine could take an instruction in English, about the wish that one could. Moving work across an interface, Dijkstra argues, does not divide a fixed amount of labor: the work of communicating across it is added, often on both sides. Dijkstra calls formal notation a privilege: with it, schoolchildren do what once took a genius. And the ease of a natural language is the ease of "making statements the nonsense of which is not obvious." It is a thousand words, but each sentence has a clause inside a clause, so read it twice. Two things to know going in: its metaphors and spellings are of its decade, and its closing remark, which blames an educational trend for a "New Illiteracy", is asserted rather than argued. That remark is also the best thing in the piece to argue with. Decide what the argument predicts about programming with an AI in 2026. About 10 minutes to read twice (cached: PDF, HTML).

Extras

Here are some additional papers that are relevant to the themes explored by the papers above, in case you are curious and want to know more. These are completely optional, but you are welcome to mention them in your reflection if you connect it explicitly to one of the papers above.

Dodds 2025, Specifications Don't Exist

Dodds works at a company that sells formal verification. The hard part, the article argues, is saying what correct means. We know how to verify a compiler. GCC is unverified only because it would cost too much. But for a web browser, or even the PDF format, no precise and coherent specification can be written. The article tells the story of Dodds's own team spending years trying to write one for PDF. Real systems have too many partial specifications that contradict each other: documents, slide decks, the system itself, and tests. The ending touches this course. A test case is a partial specification that is immediately useful, and no tool, not even an AI, can take over the work of deciding what you want. Read beside Lamport, it says why extending Floyd and Hoare to large programs is hard: there is no precise specification to prove them against. About 10 minutes to read (cached PDF).

King 2019, Parse, Don't Validate

King starts from a function that cannot be written: head, which returns a list's first element, has no answer for the empty list. The usual fix lets it return nothing. Then every caller must handle a case it often knows is impossible. When the check upstream is removed, that impossible case becomes a bug. King's fix strengthens what head accepts instead: a type for non-empty lists, so that a value carries the proof that the check was done, and removing the check makes the program stop compiling. The slogan is parse, don't validate: check the input once, at the boundary, and keep what you learned. The examples are in Haskell, with none of the notation explained, so this is the hardest read here if you have not seen it. The idea transfers to Java as a class whose constructor does the checking. Gabriel's error code that every caller must check is the kind of interface King argues against. About 20 minutes to read, longer if Haskell is new to you (cached PDF).

Regehr 2014, Use of Assertions

This is Regehr's guide to assertions. An assertion, as the post defines it, is a boolean expression at a point in a program that is true unless the program has a bug. The first rule follows from that definition. An assertion is not error handling, because a file that fails to open is not a bug. The post lists where assertions come from, among them preconditions, postconditions, invariants, and the specification: the vocabulary of our reasoning lectures. It shows them in real code, where LLVM has about one assertion per 70 lines. One story is about a Java class where a student said exceptions made assertions unnecessary, and why that is wrong. One idiom, checkRep, is a method that walks a data structure and asserts everything it can about it. It is worth knowing before we get to data abstraction. The examples are in C and C++. The cached copy also holds the 35 comments the post points to, with more stories from real code bases. About 20 minutes to read the post, and as long again for the comments (cached PDF).

Crichton 2002, Why Speculate?

Crichton, the novelist, gave this speech in 2002. The media, it claims, had turned from reporting what happened to guessing what will, and the guesses are worthless because nobody knows the future. The part people quote, the Gell-Mann amnesia effect, is two paragraphs: you read an article on a subject you know, see that the writer got it wrong, then turn the page and trust the next article anyway. Speculation is cheap, and nobody remembers when it was wrong, so nobody is ever punished for it. That goes for academics and experts too. Knowing something, by contrast, costs a great deal, and the closing story about a drug trial shows how much. The speech announces at the start that it will argue without any factual support. Some of what it then asserts, about climate most of all, did not hold up. Read it as a test of the rule it states: apply that rule to the speech itself and see what is left. It is a speech, plainly spoken, with strong language in two places. About 20 minutes to read (cached PDF).

Then read about a group that paid the cost of knowing. In 2025, METR ran a randomized study: 16 experienced open-source developers, 246 real tasks from their own projects, with AI allowed or not decided at random for each task. With AI they took 19% longer, while expecting to be 24% faster, and still believing afterward that they had been 20% faster (the study, cached PDF). In 2026 the same group said in public that its follow-up could not be trusted: developers who preferred working with AI had stopped signing up, which skewed the result (the update, cached PDF). Two short reports, about 15 minutes together.

Submit

Submit your reflection on Gradescope by Friday, October 16 at 11:59pm. The Gradescope assignment will ask you which article you read and whether you used AI for editing, and it has one box for each of the three parts of your reflection. See the readings page for more information.