In line with my desire to write about books I read, I’d like to devote this post to a book I’ve put on the back shelf for a while — E. Dijkstra’s A Discipline of Programming.

Discipline seems to be a rather excellent work. It sets out a formal framework for reasoning about programs. And not just that - it does this in the context of imperative, iterative programming, rather than the declarative or functional styles commonly upheld as the material most conducive to rigorous reasoning.

The math involved in this, however, is quite intense. There’s a lot of logic going on, and it will take me some time and paper to sort through it, internalize it, and truly understand what is going on in his symbol-pushing. A worthy endeavor, I am sure, but not at this time. I’m trying to wrap my head my head around algorithms, programming languages, and Prolog this semester — beating my brain further in my recreational time doesn’t seem prudent. I intend to revisit the book sometime (perhaps over break or in the summer), when I can take the time to go through it slowly and wrestle with its concepts until I can internalize them.

Key to Dijkstra’s reasoning framework are the well-known concepts of preconditions and postconditions, with an interesting twist: the predicate transformer. If I understand them correctly, a predicate transformer describes, for a given program and postcondition, the weakest precondition which must be met for the program to terminate with the postcondition met. Essentially, it is reasoning about a program backwards — describe its behavior by what conditions it places upon an input to achieve a desired output. A fun concept. For another day.