Re: PVS GPLed

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