Great OSQ

Back from OSQ (Santa Cruz is a Good Thing) so now crunching on a term project, Oakland/W2SP talks, the parlab demo, and finding a place to live. Odd how not sleeping outside is fairly low on the list of priorities.

Perhaps the most interesting talks were Neil's and Peter's on the BOOM project where they've been experimenting with modal extensions to Datalog (time and/or location) as means to compiling declarative programs into distributed ones. A big motivation has been their work on declarative networking, applied to tasks like synthesizing CHORD, and their current work seems to be in a similar vein -- they can synthesize and potentially verify tricky protocols. It'll be interesting to see how this transitions from framework/protocol building to their goal of general application building. Another project briefly presented was Thorn (OOPSLA09, POPL2010) which takes a similar scripting position but trades in the declarative core for actors and gradual typing -- I've been more on this side for awhile (dealing with stratification etc. at a low-level is odd), but as observed in BOOM, I think we need a bit more abstraction help in handling modality. An interesting example of such an extension is Swarm's ability to move a thread of control to a particular location (e.g., the data's).

Much of the rest of the retreat was the usual symbolic execution for concurrency and security checking stuff (where are the correct-by-design people??). It was interesting to see Prateek et al take what Raluca and I had been hacking on a couple of years ago and take it to the next level, they seem to be getting a lot of traction! They were hit by the same event explosion problem so might be worth integrating our solution in, and the problem I've been most worried about -- server interactions -- still seems to be open. Prateek avoided it by scaling down the problem (client interactions) and assuming cooperation with the server (known login, stateless server or known reset, ...).


There was a lot of grumbling about impact and fundamental process from the verification crowd so I gave a short talk on sociology. It was about using insights from 'diffusion of innovation' studies to examine the social process of applying verification (my particular interest is in doing this for PLs, but that's for another day). Unfortunately, it was partially misunderstood by some: making our research tools popularly used is nice, but not what I was advocating, and I even agree with the seemingly contrarian position that research adoption shouldn't be an academic's focus. However, the sociology community has essentially given us criteria for what it means to be a socially acceptable innovation: I'm not advocating focusing research effort on deployment but deployability. What is an appropriate verification process? We might be making bad assumptions about what people can and cannot do and thus not only running the verification race one-legged but potentially may even be in the wrong race.