pre-POPL: PLPV

I attended the workshop on "Programming languages meet program verification" on the day before POPL. There were a whole bunch of interesting meetings on the same day, so it was a tough choice, but it turned out to be a good choice.

The invited lecture was given by Manuel Fahndrich from MSR in Redmond. The talk added to my already high opinion of Manuel - it was really wonderful. He described his post-Spec# work :-) Rather than extend the language, his idea is to provide a very simple Contract class, by which the code can specified. The specifications are written in the programming language itself, e.g. Contract.Requires(e) and Contract.Ensures(e), where e is a C# expression. (His examples were in C#, but he also showed some code in VB. The recent extensions in VS 2008, such as lambda expressions, help here.) The code is then compiled to, in this case, MSIL. It's at this point that Manuel's tool kicks in, which then goes to work on the IL code, figuring out where the pre- and post- conditions are; reconstructing the expressions and then either performing a static check on them, or baking in the assertions so they occur at run-time. Also interesting was that he did the static checking using abstract interpretation rather than using a theorem prover, as in Spec#.

This was very nice. The real advantage is that they haven't extended the language at all, so they don't have to invest any time in compiler work, tools, etc. and they can concentrate their efforts on the MSIL munging. The other advantage is that MSIL is a common intermediate language, so this could work for other .NET languages, eg. VB, C++. All of these techniques could work for JVM-based languages too.

I left this talk wondering whether Matt and I ought to think about this wrt our work on separation logic. One of the possible weak-links in Manuel's work is that they have an unsound heap abstraction, also they have a rather naive handling of inheritance. Another thing that needs doing is seeing whether Manuel's techniques would work for F#. The MSIL emitted by the F# compiler is quite different to the sort emitted by C#. So I suspect they'd need to do some work with their analysis to handle this. The hope might be that things will get easier, as there should be less state-minging code. Moreover, the F# emits highly predictable MSIL code (a fact it took me ages to realize and appreciate this - I now think it's a master-stroke by Don) which would also help their tool. too many ideas, too little time...

We then had two CMU-type-theory-talks in a row :-) The type-theory du jour at CMU right now seems to be polarized type theory. I heard some of this when Bob Harper was visiting MSRC, although I was a little rusty during the talks :-( Anyhow it seems that this type theory can give a fresh insight into problems with union types, and the value restriction. This seems very nice - I've blogged before about Alex Summer's PhD that has another account for the value restriction wrt callcc. I was left wondering what the connection might be.

Kenn Knowles then spoke about some improvements to simplistic approaches to refinement types (which he referred to as "contract types"). The chief problem he wanted to address is that which techniques based on using theorem provers, it's a little unpredictable whether your program will typecheck or not - you're at the whim of the TP. The idea is to figure out where you can use other techniques - e.g. fancy existentials - to get back to a more predictable system. I'd really like to consider this wrt my work on M/Oslo with Andy Gordon.

Tom Schrijvers gave a nice talk about added type invariants to Haskell. He gave a particularly nice description of the current (version 6) type system of Haskell. Whilst I like what he did, I kind of wonder whether Haskell [which I do believe to be God's own language] is going in the right direction. Or rather, whether they shouldn't just bite the bullet and become a lazy version of Coq. The power of the system that Tom presented was pretty terrifying, and as one of the questioners noted, it's now the case that programmers have to do alot (e.g. provide proofs...)

Aaron Stump gave a really nice talk about Guru - which is a language I need to check out.

In the evening we went on a long and cold walk to find a bar. After a couple of beers, Andrew, Claudio, Johannes, Barry, Christian and I had a very nice meal at 49 Bistro.