A nicely argued article, but I haven't come across anti-Dijkstra sentiment before, so I didn't realize it needed a response. Are there many folks out there who consider Dijkstra "out of touch with reality", or was this just one wack-job on a mailing list?
Generally, mention anything Dijkstra and you get the quick smackdown. And this has been going on since he was publishing. There was a big brouhaha when he was publishing that what he was proposing in the way of programming training wouldn't work because they were not culturally acceptable (?).
Here's an easy way to determine "reality". Find a large C program. Rewrite it so that none of the loops use break. How excited will the program's maintainers' be to receive your patch?
I know that the article is foremost about Dijkstra, and uses Hoare-style verification of programs as an example only, but there's a C function with "break;" being verified using Hoare logic right there:
Presumably exceptions were not a standard feature in programming languages when Dijkstra made his comment about premature-loop-exits. The "break;" C construct is only a restricted form of exception and exceptions are much better understood now than then. Verifying a program that uses them is no more difficult than verifying a program that doesn't.
Pascal: I used to sign my comments on this site and after a polite argument I changed my ways to fit in better. It's just not the house style on news.yc.
It falls so far outside of day to day programming, that it feels somewhat alien.
I however miss the argument a bit, as i can imagine a mechanical transform that can turn the premature exit version into one without. (using if statements to remove all operations until the end of the loop)
I agree that it's pretty easy to transform the code. You could also take the code block in the loop, make it a separate function, and return instead of break. It's no harder to understand a block with break statements than it is to understand a function with multiple returns, although maybe Dijkstra wasn't a big fan of multiple returns, either.
Good thinking on both counts. Multiple returns are another limited form of exceptions, and you don't need to go back in time to ask the Dijkstra from that period if he disliked them. They too escaped theoretical treatment as it was formulated at that time :)
I have put some example rules to introduce exceptions in Hoare logic at http://snipt.org/lWg (I needed monospaced fonts, sorry for the inconvenience)
16 comments
[ 2.9 ms ] story [ 55.9 ms ] threadSome examples are http://news.ycombinator.com/item?id=477177 or http://www.catonmat.net/blog/edsger-dijkstra-discipline-in-t..., both the article and the comments. I could go on.
And I would bet that if you watch this space you will see more of the same.
I cannot imagine that somebody with at least rudimentary education in CS would concur with such a judgement.
http://frama-c.cea.fr/jessie_tutorial_index.html
Presumably exceptions were not a standard feature in programming languages when Dijkstra made his comment about premature-loop-exits. The "break;" C construct is only a restricted form of exception and exceptions are much better understood now than then. Verifying a program that uses them is no more difficult than verifying a program that doesn't.
Pascal Cuoq
Still, this submission is getting the attention it deserves, the other did not :-(
I however miss the argument a bit, as i can imagine a mechanical transform that can turn the premature exit version into one without. (using if statements to remove all operations until the end of the loop)
I have put some example rules to introduce exceptions in Hoare logic at http://snipt.org/lWg (I needed monospaced fonts, sorry for the inconvenience)