Re: [mizar] PVS GPLed

[Freek Wiedijk <freek@cs.ru.nl>]

Bob:

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

This is a very interesting quote, thanks for posting it!

So do I understand it correctly that this is not about
users not knowing how to deal with the GMP source code in
a proper way (related to users not knowing how to deal with
Mizar source code in a proper way), but instead about many
compilers having bugs that make them not compile the GMP
source code correctly (and therefore it is unrelated to
the issues of the Mizar source code being "free")?

Unrelated to this: I always claim that bugs in proof
assistants are like compiler bugs, and are therefore not a
serious reason for worry.  But this quote seems to suggest
that compiler bugs _are_ a serious reason for worry!

Freek