The Humble Programmer

This weekend I spent an enjoyable 15 minutes reading Edsger Dijkstra's 1972 Turing award lecture, entitled "The Humble Programmer". It is an entertaining collection of stories, advice, and philosophizing from one of the pioneers of theoretical computer science. The most relevant piece of advice from a more modern programming language perspective is "... the requirements 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." Even when not strictly using Hoare Logic to reason about code, the advice is good. Indeed, my advisor seems to have this ingrained in his programming. Much of his code is instrumented with invariants. He asked me last week why a particular list of inference rules for eta-expansion of a term terminates. While the termination seemed so clear I didn't even think about it before, actually finding a measure of termination helped me understand the judgment better.

A nice observation is that we should "restrict ourselves to the subset of the intellectually manageable programs". This made me smile. On the one hand it seems obvious. How could we do otherwise? But then recalling a few of the programs I myself have written, I felt chided and humbled. The thing I liked most about the paper is the respect for the difficulty of programming. His last paragraph is worth repeating: "[The computer] has already taught us a few lessons, and the one I have chosen to stress in this talk is the following. We shall do a much better programming job, provided we approach the task with a full appreciation of its tremendous difficulty, provided that we stick to modest and elegant programming languages, provided that we respect the intrinsic limitations of the human mind and approach the task as Very Humble Programmers."