On Mon, 15 Sep 2008, Robert Boyer wrote:
I was having a daytime nightmare about a possible world in which some versions of a hypothetically liberated Mizar reported that something was a theorem while others said that it was not.
There is no need to liberate Mizar for that - it is reality (and sometimes a nightmare) - all sufficiently complicated software is (sometimes) buggy. And I also don't think that open-sourcing automatically produces more incompatible versions. Especially the Mizar library is a strong reason for staying compatible in this case.
Josef