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...
What is often missing from these goto discussions is the dialog between Knuth and Dijkstra on this topic.
There is another discussion between the two of them about a problem requiring no less than four stacks to understand.
Every time this comes up, I always encourage people to read an excellent analysis by David Tribble "Go To Statement Considered Harmful: A Retrospective" that goes over Dijkstra's essay line by line and explains what it means in a more modern context: http://david.tribble.com/text/goto.html It really should be required reading in CS programs.
I've used and still use goto in the few niches it makes sense to, primarily error handling and multi-level break in C/C++.