Occasional thoughts and updates about the world of interactive theorem-proving.
16 September 2008
Ex nihilo
I’ve created this blog so as to give myself an OpenID. But I suppose it’s just possible I’ll become seduced by the whole interface and use it for more than just that.