4 ms·

I only think about "Out of the Tar Pit".

by _pmf_ 6y ago

joe_fishfish 6y ago
Fourteen years later, I still think about this. I have three half-written drafts of blog posts about things this essay has inspired me to do. I think part of the mystique of it is that the authors kind of faded into the background after publishing it. I've never been able to find a follow-up paper from them.
yboris 6y ago
It's super great! I loved it. Hope to re-read in a year or two as a reminder. https://github.com/papers-we-love/papers-we-love/blob/master/design/out-of-the-tar-pit.pdf https://github.com/papers-we-love/papers-we-love/blob/master...
akkartik 6y ago
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. Link to the paper, for convenience: http://curtclifton.net/papers/MoseleyMarks06a.pdf http://curtclifton.net/papers/MoseleyMarks06a.pdf. I think it's a siren and takes away attention that could be spent on better papers.
- nordsieck 6y ago
  > 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.
  - akkartik 6y ago
    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-methods 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.

I only think about "Out of the Tar Pit".

by _pmf_ 6y ago

I only think about "Out of the Tar Pit".

Fourteen years later, I still think about this. I have three half-written drafts of blog posts about things this essay has inspired me to do. I think part of the mystique of it is that the authors kind of faded into the background after publishing it. I've never been able to find a follow-up paper from them.

yboris 6y ago

It's super great! I loved it. Hope to re-read in a year or two as a reminder. https://github.com/papers-we-love/papers-we-love/blob/master/design/out-of-the-tar-pit.pdf https://github.com/papers-we-love/papers-we-love/blob/master...

akkartik 6y ago

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. Link to the paper, for convenience: http://curtclifton.net/papers/MoseleyMarks06a.pdf http://curtclifton.net/papers/MoseleyMarks06a.pdf. I think it's a siren and takes away attention that could be spent on better papers.

nordsieck 6y ago
> 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.
- akkartik 6y ago
  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-methods 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.