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.

Here is the crux of the argument: Translating programs from one language to another, changes their correctness when self-references is involved.

Context-Dependent Functions: arxiv.org/pdf/1501.03018

This feel like an appropriate time to bring in Douglas Hofstadter and Metamagical Themas.

I immediately though of his question: How would you translate the following sentence to Chinese: "This sentence is in English"

Having done some translating long ago, I can answer that question: it depends on context. You need to figure out what the role of "English" is in this context, and then pick one out of mainly three options:

• Keep "English"
• Replace by "Chinese"
• Reformulate the surrounding paragraph to convey the intended message in a different way.

For sure - the point about the sentence is recognizing that its self-referential, and how that creates a new meaning not purely conveyed by a direct translation of the words. I thought that was interesting relating to:

Here is the crux of the argument: Translating programs from one language to another, changes their correctness when self-references is involved.

The crux of a universal computer is that you can write an interpreter for any programming language in any Turing Complete programming language. The halting problem is just a mathematical truth, and it is equivalent to Gödel’s Incompleteness Theorem.

• if you need to run program and wait for it to finish to know whether it halts or not (sync) – language of test implementation and running it in different process/machine - is irrelevant.
• if you think you can tell just by analyzing source code (async): if program involves any outside data – there is always a chance an irreducible computation is required, which can be done only by running program, goto 1.