Re: [mizar] PVS GPLed

[Jesse Alama <alama@stanford.edu>]

Josef Urban <urban@ktilinux.ms.mff.cuni.cz> writes:

> 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.

It's possible that if mizar is open-sourced, we would see forks.  People
would continue to work on mizar, of course, but new projects based on
mizar, that do substantially the same thing, would emerge.  A famous
example of forking is the emacs/xemacs split.  See, for example,
http://www.xemacs.org/About/XEmacsVsGNUemacs.html .  The emacs editor
has a number of guises; there's also TeXmacs (http://www.texmacs.org)
and sxemacs (http://www.sxemacs.org).  Forking may lead to schism:

  http://www.sxemacs.org/docs/faq/Q1_002e0_002e5.html#Q1_002e0_002e5

I'm not sure whether that's a bug or a feature of forks.

Imagine this kind of thing taking place with mizar!

Jesse

-- 
Jesse Alama (alama@stanford.edu)