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