Classic Dijkstra:

Sad remark. Since then we have witnessed the proliferation of baroque, ill-defined and, therefore, unstable software systems. Instead of working with a formal tool, which their task requires, many programmers now live in a limbo of folklore, in a vague and slippery world, in which they are never quite sure what the system will do to their programs. Under such regretful circumstances the whole notion of a correct program – let alone a program that has been proved to be correct – becomes void. What the proliferation of such systems has done to the morale of the computing community is more than I can describe. (End of sad remark.)

This is from “a discipline of programming” which, besides being a clear tutorial on Dijkstra’s formalism, is one of those books that changes how you think about solving problems – and about computation in general. You need to be comfortable with mathematical and symbolic language, but it’s worth the time and effort.

I can’t fully get behind Dijkstra’s stringent, almost ascetic approach to programming. It’s clear that we can achieve a lot without formal methods, and that until we have powerful language support, it will be hard to use serious formalism successfully in projects of the scale we habitually undertake now. Nevertheless, he’s one of my heroes. We need these extreme and deep voices to remind us that despite our accomplishments, we’re at the very beginning of all this and we have a long way to go.

I highly recommend browsing the E. W. Dijkstra Archive. Dijkstra believed in maintaining a lively correspondence with his peers, and his EWDs make great reading.

“But what good are formal methods? You know, in many cases, formal methods are just rubbish. Sometimes one gains more from simply having a friendly chat. Oh, the formal methods will always be with us, sir, you may be assured of that; but what good are they, in the last analysis, I ask you?” – Porfiry Petrovich, from “Crime and Punishment”.