Something went wrong. Try again.
my forest
Something went wrong. Try again.
12345678\date{2025-09-19}\author{liamoc}\title{Against "eureka steps"}\p{Both [[hoefner]] and I enjoyed [[tomschrijvers]]' talk at the [[loc-001U]] answering a challenge from [[brunooliveira]]: to stepwise \em{derive} his [QuickSub](zhou-oliveira-2025) efficient iso-recursive subtype checking algorithm from the exponential-time Amber rules of [[lucacardelli]]'s #{\mathcal{F}_{<}}. Impressively, [Tom](tomschrijvers) 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 \em{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".}\p{It led me to wonder about the myriad of possible choices available at any given step in that refinement. Why do we choose \em{this} algorithm? If I recall some of the classic works on program calculation from [[richardbird]] or [[ccm]], 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. }\p{I encountered a similar feeling when my student [[xinloi]] raised [[raad-bdo-2022]] for discussion with me and [[hoefner]]. [[ohearn-2020]] 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 \em{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, [[raad-bdo-2022]] 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](tomschrijvers)'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. }