Operational Reasoning

An even stronger claim than StopUsingMetaphors, belongs also to EwDijkstra: avoid OperationalReasoning like the plague. And you have to think that he meant operational reasoning as a mathematical activity, whereas in real life people do their operational reasoning in metaphorical terms.

I have been unable to locate a definitive explanation for OperationalReasoning, so I'm left with conjecture. Anyone want to stack their conjecture up against mine? -- GarryHamilton

Operational reasoning means reasoning about the programs by thinking how a machine executing the program will run: what effect on the state of the machine will each instruction have, what will program do next, etc. Simulating the processor (or an abstract interpreter) in your head.

Ahhh, I see. The sort of thing that we do in EmbeddedSystems all the time. I guess when adequate resources are in play, one is free to think in the abstract without worrying about which register has the bean and what segment of memory is affected and how that will impact LRU caching schemes and RealTime event processing.

If what you're doing is sufficiently aloof from the hardware, then OperationalReasoning works against you. If you're directly concerned with bus activity and bit phases and register vs stack usage for resource conservation, the OperationalReasoning isn't optional, it's necessary.

Thanks. -- GarryHamilton

I believe it is a matter of choosing the right 'machine'. The hardware is just one of the possible 'machine' models to reason against, but there are more abstract models. Or are we talking about denotational reasoning as an alternative? Somehow I have a hard time imagining mere mortals reasoning about their programs in terms of fix-points. (Alternative reasoning schemes and examples are welcome.) -- cristipp

I don't see what's so hard to imagine, especially since you were imaginative enough to bring it up. One example: "Fixed Point Theorems in Logic Programming" http://www.drkhamsi.com/publication/fpplogic.pdf.
Fixed point reasoning has also been used (as I've mentioned before) to reason about halting (convergence) vs non-halting (divergence) in Turing machines, and in many similar areas. Banach spaces are a handy tool. -- DougMerritt
See also the (in draft, unpublished) "Design Concepts in Programming Languages" http://cs.wellesley.edu/~fturbak/pubs/6821/ with table of contents online at http://cs.wellesley.edu/~fturbak/pubs/6821/contents.pdf and note chapters:
- chapter 3: operational semantics
- chapter 4: denotational semantics
- chapter 5: fixed points

I use 'reasoning' in the sense of the everyday activity that all programmers engage to ensure their programs work as expected. When I design a piece of code I run a little abstract machine in my head, not a fixed-point theorem prover. I find it hard to believe that your everyday programmer of choice does otherwise.

Duh. Of course. Your everyday programmer doesn't even know any higher mathematics (nor do they do e.g. logic programming). You're changing the question.

This page states 'avoid OperationalReasoning like the plague', while defining OperationalReasoning as reasoning about the execution of little abstract machines in one's head. I was merely trying to see how the advice applies to me, an everyday average programmer.
You missed or forgot the context, above, of StopUsingMetaphors, and that this is about EwDijkstra's thoughts. As a formalist he was big on proofs, and deplored the practices of the "everyday programmer" (which doesn't seem to mean you, since you know enough to raise the issue of fixed points), specifically including use of OperationalReasoning. So the starting point was, basically, assuming that programmers usually do only OperationalReasoning. And as we all know, programmers typically do not do proofs, but EwDijkstra wants them to.
As for the practical issue of how the advice applies to you/us, that's a good question. I think ProofCarryingCode would be one possible answer.
- If I remember correctly, ProofCarryingCode deals with operational semantics.

However, it's probably true that every formalized approach to reasoning has an informal intuitive counterpart that is regularly used by the unschooled, and that is certainly true of fixed points (and of OperationalReasoning, see e.g. the wikipedia definition).

I'm genuinely interested in seeing the intuitive counterpart for denotational reasoning. Would you please oblige? (examples welcome).

Examples of non-operational approaches.

Denotational is not the only alternative to operational. The other major alternative is axiomatic semantics, which would correspond to proof driven design / correctness by construction. Unfortunately, proof-driven design has fallen a bit in popularity. However, books like DisciplineOfProgramming, TheScienceOfProgramming, have plenty of examples to get you going. EwDijkstra papers (the EWxxxx series) that deal with programming problems and techniques all use this style of reasoning. The classic paper "On the fly garbage collection, an exercise in cooperation" is a beautiful demonstration that, in the hands of experts, the technique scales to difficult problems. Actually, it may be the only technique that can deal with concurrent and distributed programming effectively. There's the book Parallel Program deisgn by Misra and Chandy, and A Discipline of Multiprogramming by Misra, each of those have plenty of examples.

Using this terminology, ProofCarryingCode would be categorized as axiomatic. Hoewever, the implementation mechanism (as far as I can tell) is an abstract interpreter running over a formula domain, yielding a verification condition formula which is later proved using plain first order logic. Does the interpretor in it make for an 'operational' approach over a more sophisticated domain?

ApplicativeCommonLisp? is also a very interesting environment for reasoning about programs in a non-operational way. It has been used in some industrial projects and it's very easy to get started with because it's basically Lisp -- (theorem proving). Not only that, but there's currently a good environment for Eclipse (tested, it works) and another one for DrScheme (have yet to test). It's extremely fun to program in, the pesky theorem prover keeps telling you that you have to prove that your recursion terminates. It's bloody obvious to you that it "should" terminate, but convincing a prover/verifier is quite different, challenging and sometimes insightful.

For denotational reasoning (thinking in terms of the "denoted" objects, in the denoted universe, rather than about the interpreter for the language), this is by default, the style of thinking in HaskellLanguage (see The EvolutionOfaHaskellProgrammer?, of course :). A very nice book about thinking in terms of functions (and relations) compositions and properties thereof is AlgebraOfProgramming.

There are many other examples, that I have no direct experience with. The problem with aby abd all non-operational approaches to thinking about programs is that it requires a non-trivial learning investment. And it starts with EmptyYourCup, if you want to make any progress. That's the sense of Dijsktra's "avoid operational reasoning like the plague".

Currently, there's the VerifyingCompiler "grand challenge" being proposed by TonyHoare and JayadevMisra?. If it's going to be solved it will most likely not involve operational reasoning (I know of no popular theorem prover/verifier that works with operational semantics).

I remember that in one of the papers Dijkstra didn't say to always avoid operational reasoning, advised people not to have that as their only option, and said that it was his justification for hating anthropomorphic metaphors. He gave the example of proving that it's not possible to cover a 8x8 square with one pair of opposite corners removed with dominoes. The operational method would be to exhaustively try all of the possible ways of placing dominoes down. His suggestion was that instead, the squares should be coloured like a chessboard, and then it can be seen that, since every domino covers a white square and a black square, and the squares on opposite corners are the same colour as each other, there are therefore 30 squares of one colour and 32 squares of the other, proving the dominoes can't be placed on there. Although he didn't say this, I believe what he was driving at was that instead of defining every case a program can be used in and exhaustively testing them all, one can potentially achieve easier results by adding some form of annotations and using proof. However, I could be wrong. (EWD1036 at http://www.cs.utexas.edu/~EWD/transcriptions/EWD10xx/EWD1036.html - near the end)

See

MarchZeroSix