3 ms·

> But the users are all mathematical enough to want formal requirements. This seems like a strange interpretation. I understand that the term "formal requireme

> 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.

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.