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 software that is simple to build spreads and wins, even when it is not quite right, and can be made right later. Lamport says a program is a mathematical object, so a programmer can ask what it means and whether they could prove it. Dijkstra says the formal care is the point, and that wishing 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, and this is a section of his longer essay on Lisp. It names two ways to design software. The MIT way, which he calls "the right thing", puts the interface first: simple, correct, consistent, and complete, whatever that costs the implementation. The New Jersey way puts the implementation first and lets the people who use it do the extra work. Gabriel caricatures the second on purpose, then argues that it won: Unix and C gave people half of what they wanted and were easy to port, so they spread everywhere. His advice is to ship half of the right thing, as long as that half is basically right, and improve it once people depend on it. About 10 minutes to read (cached: PDF, HTML).

Lamport 2003, The Future of Computing: Logic or Biology

By "logic", Lamport means Floyd and Hoare's idea: a program is a mathematical object, so you can ask what it means and whether you could prove it means that. He is not asking anyone to write that proof, only to ask themselves whether they could. By "biology", he means how programs are treated now: as mysterious as the human body, so met with superstition (avoid whatever crashed last time) and left to evolve and fight off viruses. That road gives up on understanding software at all, and software nobody understands cannot be made dependable. His way back is to keep systems simple enough to understand, with logic as the tool. About 20 minutes to read (cached: PDF, HTML).

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

Dijkstra wrote this about the wish for a machine you could instruct in English. Moving work across an interface, he argues, does not divide a fixed amount of labor: the work of communicating across it is added, often on both sides. Formal notation is a privilege, since 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." His closing guess is that machines programmed in English would be as hard to make as to use. About 10 minutes to read (cached: PDF, HTML).

Extras

These are optional. You may bring one into your reflection if you connect it to the article you chose.

Dodds 2025, Specifications Don't Exist

Dodds works at Galois, which sells formal verification. The hard part, he 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: a real system has too many partial specifications, in documents, slide decks, the system itself, and tests, and they disagree. His own team spent years on a formal specification for PDF and ended with one that matches neither the existing readers nor what a PDF ought to be. A test case is a partial specification that is immediately useful, and that is the kind to build on, since "even Claude can't tell us what to want." About 10 minutes to read (cached PDF).

King 2019, Parse, Don't Validate

King starts from head, which returns a list's first element and so has no answer for the empty list. The usual fix lets it return nothing, and then every caller must handle a case it often knows is impossible; when the check upstream is removed, the impossible case becomes a bug. King's fix strengthens what head accepts instead: a type for non-empty lists, so a value carries the proof that the check was done, and removing the check makes the program stop compiling. That is the slogan: a validator checks and throws the knowledge away, and a parser checks and keeps it in the type. King's practical advice is to use data structures that make illegal states unrepresentable, and to parse at the boundary of the system, before any of the data is acted on. The examples are in Haskell. About 20 minutes to read (cached PDF).

Regehr 2014, Use of Assertions

Regehr's post is a guide to assertions. An assertion, by the definition he uses, is a boolean expression at a point in a program that is true unless the program has a bug, so an assertion is not error handling: a file that fails to open is not a bug. He lists where assertions come from, among them math, preconditions, postconditions, invariants, and the specification, and shows them in real code, where LLVM has about one per 70 lines. The one bad mistake is an assertion that changes the program's state, since the program then behaves differently with assertions on and off. One idiom, checkRep, walks a whole data structure and asserts everything it can about it. A student once told him exceptions made assertions unnecessary; his better answer is that exceptions are a mechanism, and assertions and error handling are two different things built on it. The examples are in C and C++. About 20 minutes to read (cached PDF).

Crichton 2002, Why Speculate?

Crichton, the novelist, says the media had turned from reporting what happened to guessing what will, and that the guesses are worthless because nobody knows the future: pundits do no better than chance, and expertise is no shield. He names the Gell-Mann amnesia effect: 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 thrives, he argues, because it is cheap and nobody remembers when it was wrong, and that holds in academia too, where speculation is called theory. He announces at the start that he will argue without any factual support, and closes with a drug trial whose protocol shows what reliable knowledge costs. It is a speech, with strong language in two places. About 20 minutes to read (cached PDF).

METR 2025 and 2026, two productivity studies

In 2025 METR ran a randomized trial: 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 group reported that its follow-up gives an unreliable signal: the raw numbers show a speedup, but developers who did not want to work without AI had stopped signing up and stopped submitting tasks, which biases the estimate down, so the group calls the data weak evidence and is changing the design (the update, cached PDF). 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.