Re:Goto (2007)
by User23 on Saturday October 23, 2021 @02:36PM
(#28971076)
> "Dijkstra later abandoned the search for program provability and turned instead to the study of techniques for correct program derivation"
It's odd how even today very few people in the "formal verification" world understand this distinction. Naturally verifying a derived program is trivial, since it's literally a proof by construction. I've attempted many times to explain this distinction, and they inevitably just start babbling about the limitations of the tooling they use. A sad case of man with a hammer syndrome and probably an illustration of my own failure to achieve clarity I guess.
> "However, to some extent Dijkstra's principle has not been fully realized when we observe the complexity that must be dealt with by real-world programming tasks, such as multitasking, multithreading, interrupt handling"
Dijkstra designed the first proven correct interrupt handler for a multitasking OS two years before the Goto Letter[1][2] so I think we can rest assured that he was aware of these issues.
It's odd how even today very few people in the "formal verification" world understand this distinction. Naturally verifying a derived program is trivial, since it's literally a proof by construction. I've attempted many times to explain this distinction, and they inevitably just start babbling about the limitations of the tooling they use. A sad case of man with a hammer syndrome and probably an illustration of my own failure to achieve clarity I guess.
> "However, to some extent Dijkstra's principle has not been fully realized when we observe the complexity that must be dealt with by real-world programming tasks, such as multitasking, multithreading, interrupt handling"
Dijkstra designed the first proven correct interrupt handler for a multitasking OS two years before the Goto Letter[1][2] so I think we can rest assured that he was aware of these issues.
[1] https://en.wikipedia.org/wiki/THE_multiprogramming_system
[2] https://www.cs.utexas.edu/users/EWD/transcriptions/EWD01xx/E...