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:
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
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.
What effect is there on optimization?