Here is Dijkstra himself answering the charge via EWD288 - "Concern for Correctness as a Guiding Principle for Program Composition". Finally, a word or two abo

Here is Dijkstra himself answering the charge via EWD288 - "Concern for Correctness as a Guiding Principle for Program Composition". Finally, a word or two about a wide-spread superstition, viz. that correctness proofs can only be given if you know exactly what your program has to do, that in real life it is often not completely known what the program has to do and that, therefore, in real life correctness proofs are impractical. The fallacy in this argument is to be found in the confusion between "exact" and "complete": although the program requirements may still be "incomplete", a certain number of broad characteristics will be "exactly" known. The abstract program can see to it that these broad specifications are exactly met, while more detailed aspects of the problem specification are catered for in the lower levels. In the step-wise approach it is suggested that even in the case of a well-defined task, certain aspects of the given problem statement are ignored at the beginning. This means that the programmer does not regard the given task as an isolated thing to be done, but is invited to view the task as a member of a whole family; he is invited to make the suitable generalizations of the given problem statement. By successively adding more detail in the lower levels he eventually pins his program down to a solution for the given problem. You can also find some relevant discussion (including my posts) at https://news.ycombinator.com/item?id=24942671 https://news.ycombinator.com/item?id=24942671 The point is that by using a top-down and step-wise refinement methodology one can show "correctness" at whatever level of granularity is acceptable.