I've never understood why people like this paper. Over the years I've evolved a bite-sized rebuttal, if anybody wants to fight me:
The authors' "ideal world" is one where computation has no cost, but social structures remain unchanged, with "users" having "requirements". But the users are all mathematical enough to want formal requirements. The authors don’t seem to notice that the arrow in "Informal requirements -> Formal requirements" (pg 23) may indicate that formal requirements are themselves accidental complexity. All this seems to illuminate the biases of the authors more than the problem.
> But the users are all mathematical enough to want formal requirements.
This seems like a strange interpretation. I understand that the term "formal requirements" has a technical meaning in some disciplines, but I also think it's pretty clear that the author isn't using the term in that way.
It is much more likely that the author meant that users have requirements, but those requirements don't typically map cleanly to actions taken by the computer. This step of translation is necessary in the construction of a program, even if it is typically done piecemeal and iteratively.
It's a strange interpretation only if you focus on just the vocal minority that talks about formal requirements. Here are two quotes by Hillel Wayne (https://www.hillelwayne.com/post/why-dont-people-use-formal-...), whom I've found to have the most balanced take:
"The problem with finding the right spec is more fundamental: we often don’t know what we want the spec to be. We think of our requirements in human terms, not mathematical terms. If I say “this should distinguish parks from birds”, what am I saying? I could explain to a human by giving a bunch of pictures of parks and birds, but that’s just specific examples, not capturing the idea of distinguishing parks from birds. To actually translate that to a formal spec requires us to be able to formalize human concepts, and that is a serious challenge."
"It’s too expensive doing full verification in day-to-day programming. Instead of proving that my sort function always sorts, I can at least prove it doesn’t loop forever and never writes out of bounds. You can still get a lot of benefit out of this."
The post makes a strong case, IMO. Formal methods can be valuable, but they don't have the track record yet for anyone to believe they're the #1 essential thing about programming.
The authors' "ideal world" is one where computation has no cost, but social structures remain unchanged, with "users" having "requirements". But the users are all mathematical enough to want formal requirements. The authors don’t seem to notice that the arrow in "Informal requirements -> Formal requirements" (pg 23) may indicate that formal requirements are themselves accidental complexity. All this seems to illuminate the biases of the authors more than the problem.
Link to the paper, for convenience: http://curtclifton.net/papers/MoseleyMarks06a.pdf. I think it's a siren and takes away attention that could be spent on better papers.