Day 2 opened with Benjamin Pierce summarizing his experiments in making heavy use of a proof assistant (Coq) during his CS class. Basic summary was “its hard work for the organizer, but the students appear to gain a better understanding”. More concretely, he’s shared the coursework so that other people (ie. me!) can use it without having to fly out to the University of Pennsylvania.
Next two talks were over my head; I’m always surprised that naming and binding cause so much headache for formal systems. I’ve seen De Bruijn indices used before, but they cause people to drown in unhelpful arithmetic and so people look for other ways. Anyhow, I know I know nothing about this (although Sam Lindley did give me a high level overview), so I will skip onwards.
“Finding race conditions in Erlang” was practical and interesting – trying to find internal race conditions in a service by concurrently calling its api methods in random order. Well, ‘random’ order wouldn’t be so helpful, since part of the work was to find minimal examples where the concurrent calls had behaved differently from if they’d been called serially. They use quickcheck to generate the call sequences (and benefit from its minimization features) but they had to hook the Erlang VM at various points so they could control the scheduler and get some modicum of repeatability during their runs.
“Partial memoization of concurrency and communication” was more interesting than the title suggested. Memoizing pure functions is pretty easy – you do the work once, and stash the answer in a cache keyed off the argument values. However, for side-effectful computations this doesn’t work, since getting the right answer out without performing the side effects just ain’t the same thing. So, the idea was to track the side effect (specifically, message sends/receives in CML) and attempt to re-enact those interactions in a kind of ‘replay mode’. If all the interactions could be carried out just like in the original run, great, you can return the final answer and you’re done. But if the replay fails part way through, you can resume the execution of the original code (a continuation) from that point and at least you saved some work.