A few quotations summarizing Dijkstra's POV:

``... by admitting —or should we say: by generating?— the possible computations into our considerations we open the door to a combinational explosion, the effect of which quickly defies exhaustive analysis.''

``The postulational method deals with the program text as a parsed but otherwise uninterpreted formula.''

In Dijkstra's view one half of programming is coding a program, and the other half is demonstrating that the program satisfies some desired specification (and hopefully that the program satisfies it with a minimal amount of resources).

The most common approach to programming today (as far as I can tell) is still operational, where one first writes a program, then after the fact one argues to one's satisfaction that the program satisfies the spec by walking through the program's execution (I think this is what is called operational semantics,'' which just meansexecutional meaning.'') I've done this myself...

The postulational method involves ignoring the interpretation of code as executable program and instead using formal symbol-manipulation rules to show that the code satisfies a spec. This is also called the axiomatic method when it is used in mathematics.

The axiomatic method is more abstract and easier in terms of the amount of work necessary to carry it through. Dijkstra often called upon the example of integer division as an example of the power of the axiomatic method. When performing long division, it is unnecessary extra work to remember the interpretation of digit-strings as integers while calculating. At the end one may reinterpret the strings and get an interesting result. Likewise one may manipulate program texts without continually interpreting them as executables and then at the end show that a program satisfies some spec.