Best Dijkstra papers to explain this quote?

I was enjoying "The Humble Programmer" earlier today and ran across this choice quote:

Therefore, for the time being and perhaps forever, the rules of the second kind present themselves as elements of discipline required from the programmer. Some of the rules I have in mind are so clear that they can be taught and that there never needs to be an argument as to whether a given program violates them or not. Examples are the requ开发者_如何学Pythonirements that no loop should be written down without providing a proof for termination nor without stating the relation whose invariance will not be destroyed by the execution of the repeatable statement.

I'm looking for which of Dijkstra's 1300+ writings best describe in further detail rules such as he was describing above.

Page 5 through 18: http://userweb.cs.utexas.edu/users/EWD/ewd02xx/EWD249.PDF
Mid. page 3 through end: http://userweb.cs.utexas.edu/users/EWD/ewd04xx/EWD473.PDF
End page 5 through end: http://userweb.cs.utexas.edu/users/EWD/ewd06xx/EWD641.PDF
All: http://userweb.cs.utexas.edu/users/EWD/transcriptions/EWD02xx/EWD261.html ^{(Dutch, translation=below)}

_{Note: Dijkstra numbers his pages starting at 0. Given page numbers are starting at 1, the PDF page number, and not the written page numbers.}

My translation of EWD261 in English:

How to program mathematically

A (well-defined) programme is structured just like a (well-defined) mathematical theory. The programmers' work is not different from that of a creative mathematician.

There are small, but important, differences, though:

1. There are not much basic concepts of programming and they are not difficult to comprehend (though misleadingly simple); this is why it's an ideal for development practice. (Besides this, there is the fact that a demand for correctness, the programme should really work!)
2. With most mathematical education one learns about existing theorems, viz. equipping a student with a specific (detailed) set of concepts; a programmer, however, has to develop the needed concept himself. Programming requires the abstractions which leads to a type of creativity, while the same in mathematics is limited to applying existing theorems.
3. Because programmes are big and nevertheless have to work will programmers learn how to develop carefully and consciously. This is exactly what one should teach! To teach extensive knowledge is, for me, not justified.