Re: PVS GPLed

Freek,

>> I never heard a serious explanation
>> of why the sources are closed,
>
> I know two anecdotes related to this (but maybe for you
> neither of them is serious):

Right, they are anecdotes, and they are always told in that spirit. 
Problem is that in eight years I really never heard any _serious_ 
argument, to say nothing about having a serious and rational discussion. 
Nothing to match the arguments expressed in the couple of previous 
e-mails, and told over and over in many other places (read e.g. the 
last-but-one paragraph of 
http://www.dwheeler.com/essays/high-assurance-floss.html).

> - The current policy of only getting the sources when
>  you write at least one serious Mizar article made _you_
>  write some very nice Mizar articles.  So that policy
>  payed off.

No, I can't see how anyone can claim that because I (or someone else) was 
forced to write one Mizar article, the policy paid off. That does not 
account for the damage this policy causes. For my Msc. work, I originally 
rejected Mizar right in the beginning, because I could not easily get its 
source. Then it took at least a year of useless workarounds before I was 
forced by my PhD supervisor to write the article so that I could get the 
sources. I would probably never decide to do this myself, and rather 
turned to other open-source proof assistants (I was experimenting with 
IMPS a lot at that time).

There were other people since, who struggled with reverse engineering 
Mizar (without writing any article), and also others who rejected Mizar 
because of non-openness. Obviously those who rejected it immediately are a 
bit hard to count :-).

> - The sources used to be open, but then the only effect
>  of that was that some silly person made a version of
>  Mizar that just was different in that all the keywords
>  had been changed.  That was so irritating that after that
>  the sources got closed.

I can't see what is irritating about thousands versions of Linux kernel 
being used by various people. Some of the patches will never be accepted 
into "official Linux" by Torvals/Morton, some will, some will get strong 
support from their users anyway. There are countless examples of this - 
the year is now 2008, not 1980 :-). One of them is obviously all the 
various flavours of HOL and Isabelle. It is a fairly speculative 
subject, but AFAIK this diversity and parallelism has rather fostered the 
development of HOL-based systems than not (think e.g. Isar vs. old-style 
Isabelle, Meson vs. Metis vs. Sledgehammer, the cool HTML presentation for 
Isabelle/ZF at http://formalmath.tiddlyspot.com/, etc.).

Also, last time I heard that someone in Germany did translate Mizar-MSE 
keywords to German, it was in Bialystok, and accepted positively.

Josef