Yeah I think so. My takeaway was that operational reasoning, e.g. "this guy receives a message from this guy, then does this" is a waste of effort. What Dijkstr

Yeah I think so. My takeaway was that operational reasoning, e.g. "this guy receives a message from this guy, then does this" is a waste of effort. What Dijkstra wants you to do is elevate yourself above that so you're reasoning in more powerful abstractions. I thought his analogy was illuminating of the point: "The point to get across is that if we have to demonstrate something about all the elements of a large set, it is hopelessly inefficient to deal with all the elements of the set individually: the efficient argument does not refer to individual elements at all and is carried out in terms of the set's definition."