Hi, Kartik, I'd be very interested in having a conversation about Dijkstra's book. I still have my copy that I ordered as soon as I could after it was published. Working through that book (one works it instead of reading it 🙂) profoundly changed my perspective on programming.

I find it highly ironic that some people who have been critical of formal methods (or even of Dijkstra's style and content) are also proponents of TDD. I have long thought that both ADoP and TDD emphasize using reasoning about correctness as part of the design process (although I continue to believe that Dijkstra's method is potentially more robust, for a variety of reasons).

I'm curious as to what about chapters 6 (designing for termination) and 7 (Euclid's algorithm revisited) left you uncomfortable.

I hope we can connect.

I hadn’t thought about your before-and-after interpretation in quite that way. I’ll have to ponder a bit.

Regarding your reference to determinism, only some constructions in EWD’s wp-based notation are deterministic! While some cases (e.g. x := x-y ) are, EWD’s reasoning makes some kinds of determinism a not-very-interesting special case. The “Aha!” moment for me was his solution for max in c := a max b .

if

   a >= b -> c := a

[]

   b >= a -> c :- b

fi

In the (again, uninteresting) special case that a = b , both guards are true it is perfectly valid to “perform” either of the two guarded commands.