Wednesday, April 14, 2010

You wait months for a good seminar...

...and then three come along at once!

Following Monday's seminar Robert was scheduled to talk again on tuesday, this time at the NZCSRSC (student research conference). It sounded like an interesting talk - "How to change the world" is not a modest title. And having perused the slides I am very disappointed not to have attended - it looks like there were a lot of good things, and thinking about your work in terms of impact is an interesting perspective, and one which I have not thought of since working in PLT.

Anyway, I couldn't attend because I was attending another seminar, this one from Rusten Leino on the Dafny language/verifier and other verifcation stuff going on at Microsoft research. It was a very interesting seminar with a very good demo of verification in action. Pretty impressive amount of bugs caught and all proofs done automatically - it was kind of like magic! Really solved the problem I have with a lot of these things, which is that no-one wants to prove their programs. The annotation overhead is still quite high, and I think only a minority of programmers will be able to write the specifications. But, with a little practice, I can imagine writing code with specs in Dafny in a practical way.

Rusten also summarised some of the other verification efforts he is associated with and they have acheived some pretty cool stuff.

"Dynamic framing" sounds cool, and I should try and understand it better.

Overall, I got the feeling that right there was the future of 'safe' programming languages, or at least a sneak peak of it. And, since it's at Microsoft, it actually has a fighting chance of making it into the real world!

No comments: