Re: PVS GPLed

I think an even better example of what might be "irritating" (e.g. to 
kernel hackers) is the number of malicious kernel rootkits based on their 
work. Or the large "antisocial" parts of internet "irritating" Chinese 
censors. For me, there is an infinite distance between the friendly 
warning by the GMP people, and the "Chinese solution" :-).

Josef

On Mon, 15 Sep 2008, Robert Boyer wrote:

> 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 <[email protected]>
> To: [email protected]
> 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
>
>