4 ms·

Dijkstra grappled with these issues. Two classic notes of his are: https://www.cs.utexas.edu/users/EWD/transcriptions/EWD03xx/EWD303.html https://www.cs.utexas

Dijkstra grappled with these issues. Two classic notes of his are: https://www.cs.utexas.edu/users/EWD/transcriptions/EWD03xx/EWD303.html https://www.cs.utexas.edu/users/EWD/transcriptions/EWD03xx/E... https://www.cs.utexas.edu/~EWD/transcriptions/EWD10xx/EWD1036.html https://www.cs.utexas.edu/~EWD/transcriptions/EWD10xx/EWD103... There are several takeaways here, but three of my favorite highlights: * Dijkstra actually did not like calling such errors "bugs", as it is a framing problem. * Likewise, he believed that we should avoid anthropomorphizing software or identifying with it. * Finally, he believed in building a formal specification of software and then proving that the software matched this specification. Part of this was to avoid "bug fixing" hunts in which the focus was on "debugging" instead of correctness. But also, this was to ensure that there was a proper system view of the software, which ties back into the conclusion of the article here.

rramadass 3y ago
Nice! It is a tragedy that programmers nowadays don't read Dijkstra nor think about what he wrote and meant. I tell people to think of him as their "Cus D'Amato" if they want to be a "Mike Tyson" in their field i.e. a man who has thought deeply about the subject, knows all the angles and can "train" one in the "correct" manner of writing programs.
shiandow 3y ago
Interestingly most bugs I encounter are bugs in the specification, so in some ways formal specification just moves the problem.
- nanolith 2y ago
  Formal specification means building up this specification from theory, and building proofs along the way. Of course, there can always be errors in specification, but this is supposed to be the first place we implement SAT solvers or proof assistants. During Dijkstra's time, such technologies were not yet available as they are now. There is work to be done until this is all practical and the overhead to do this is within the current overhead of software engineering, but we are quickly reaching that point in time.
Hendrikto 2y ago
> he believed in building a formal specification of software and then proving that the software matched this specification. Given unlimited time and budget, plus the guarantee that things won‘t need to change in unexpected ways, that would be great.
- throwaway290 2y ago
  The spec does not have to be infinitely precise and can exist under budget constraints.
- nanolith 2y ago
  Each of these things can be managed with process. It's not an all-or-nothing strategy. The overall system and application changes in unexpected ways, but as you get lower down the stack, the amount of churn is reduced. Hence, there are strategies to design systems and applications so the most high-assurance pieces are those least subject to change, and that the application code itself runs at the lowest assurance level. Of course, Dijkstra was more of an academic, but this can be managed in real systems with engineering process. A system that is 20% formally verified is safer and has fewer defects than one that is 0% formally verified. The key is applying engineering to this to ensure that the time and budget spent on this specification provides the most benefit.

rramadass 3y ago

Nice! It is a tragedy that programmers nowadays don't read Dijkstra nor think about what he wrote and meant. I tell people to think of him as their "Cus D'Amato" if they want to be a "Mike Tyson" in their field i.e. a man who has thought deeply about the subject, knows all the angles and can "train" one in the "correct" manner of writing programs.

shiandow 3y ago

Interestingly most bugs I encounter are bugs in the specification, so in some ways formal specification just moves the problem.

nanolith 2y ago
Formal specification means building up this specification from theory, and building proofs along the way. Of course, there can always be errors in specification, but this is supposed to be the first place we implement SAT solvers or proof assistants. During Dijkstra's time, such technologies were not yet available as they are now. There is work to be done until this is all practical and the overhead to do this is within the current overhead of software engineering, but we are quickly reaching that point in time.

Hendrikto 2y ago

> he believed in building a formal specification of software and then proving that the software matched this specification. Given unlimited time and budget, plus the guarantee that things won‘t need to change in unexpected ways, that would be great.

throwaway290 2y ago
The spec does not have to be infinitely precise and can exist under budget constraints.
nanolith 2y ago
Each of these things can be managed with process. It's not an all-or-nothing strategy. The overall system and application changes in unexpected ways, but as you get lower down the stack, the amount of churn is reduced. Hence, there are strategies to design systems and applications so the most high-assurance pieces are those least subject to change, and that the application code itself runs at the lowest assurance level. Of course, Dijkstra was more of an academic, but this can be managed in real systems with engineering process. A system that is 20% formally verified is safer and has fewer defects than one that is 0% formally verified. The key is applying engineering to this to ensure that the time and budget spent on this specification provides the most benefit.