Re: [mizar] PVS GPLed

[Robert Boyer <boyer@cs.utexas.edu>]

I tend to avoid having views about what others should
do, e.g., use the GPL or not, because it is too
difficult for me to think through.  But I cannot let
pass without comment your remark:

> I can't see what is irritating about thousands
> versions of Linux kernel being used by various
> people.

GMP is a Gnu library written in C that does bignum
arithmetic.  It is said to be quite fast.

>From the front page, http://gmplib.org/:

   GMP is very often miscompiled!  We are seeing ever
   increasing problems with miscompilations of the GMP
   code. It has now come to the point where a compiler
   should be assumed to miscompile GMP. Please never
   use your newly compiled libgmp.a or libgmp.so
   without first running make check. If it doesn't
   complete without errors, don't trust the
   library. Please try another compiler release, or
   change optimization flags until it works. If you
   have the skill to isolate the problem, please report
   it to us if it is a GMP bug; else to the compiler
   vendor. (The compilers that cause problems are HP's
   unbundled compilers and GCC, in particular Apple's
   GCC releases.)

Ever increasing!

Bob


-------------------------------------------------------


Date: Mon, 15 Sep 2008 17:24:09 +0200 (CEST)
From: Josef Urban <urban@ktilinux.ms.mff.cuni.cz>
To: mizar-forum@mizar.uwb.edu.pl
Subject: Re: [mizar] 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