Both Peter Höfner and I enjoyed Tom Schrijvers' talk at the IFIP WG2.1 Meeting #83 answering a challenge from Bruno C. d. S. Oliveira: to stepwise derive his QuickSub efficient iso-recursive subtype checking algorithm from the exponential-time Amber rules of Luca Cardelli's \mathcal {F}_{<}. Impressively, Tom and his student were able to get there, and it's certainly nice to have such a neat justification of QuickSub's correctness, but I did experience some mild irritation: The calculation was done with a very specific goal in mind — namely the QuickSub algorithm — and so several steps in the proof were, in a sense, "goal-motivated". If we didn't know the QuickSub algorithm in advance, many steps would have had no intuition behind them at all. Another member of the group called such steps "eureka steps".
It led me to wonder about the myriad of possible choices available at any given step in that refinement. Why do we choose this algorithm? If I recall some of the classic works on program calculation from Richard Bird or Carroll Morgan, the algorithms we end up with proceed from a series of calculations, each of which makes sense in isolation. You can read the derivation from beginning to end and each step feels like it's improving the algorithm in some way. The process feels entirely natural. Whereas here, these "eureka steps" mean that I need to look much further ahead to find the motivation for the transformation being performed.
I encountered a similar feeling when my student Xin Lu raised Concurrent Incorrectness Separation Logic for discussion with me and Peter Höfner. Incorrectness Logic is, in a nutshell, a logic for showing the presence of bugs rather than their absence. One of its nice qualities is that, like its almost-dual Hoare logic, it offers a relatively calculational way to approach program (in)correctness, where each proof step follows naturally from the structure of the program and the assertions within it. Unfortunately, Concurrent Incorrectness Separation Logic doesn't quite preserve this property when moving to a concurrent setting. To prove the existence of concurrency bugs like races, each thread's local assertions build a history of writes and lock actions, and then, in the assertion after the potential race, a "eureka step" comes in which points out the problematic interleaving of these histories that exhibits the race condition. Proving the presence of this bug required first knowing that the bug exists and how it can arise, and then doing the same "goal-motivated" reasoning that we saw in Tom's talk. This seems to me quite dissatisfying. Is there a more genuinely calculational approach here? I suspect concurrency makes things fundamentally more difficult, but I think we should nonetheless strive for the elimination of these "eureka steps" even if it's not always possible to do so.