In addition, Dijkstra broaches the interesting idea that proofs ought to be constructed
at the level of the flowchart first. Once that is done, using high level steps, it can be
refined into code. But the proof of the code is essentially a refinement of the proof of
the flowchart. This idea is interesting in that it is often the case that a flowchart might
say "find the largest value such that...", which when reduced to code would involve a loop.
A proof that the largest value exists at the abstract "flowchart" level would be easier
to prove than a low-level inductive proof of a program loop that implements the search
and involving issues such as finding invariants.
To my mind, this "hierarchical proof technique" (my words, not Dijkstra's) is rather
interesting.
Tim