Re: PVS GPLed

On Mon, 15 Sep 2008, Josef Urban wrote:
> There is no need to liberate Mizar for that - it is reality (and
sometimes 
> a nightmare) - all sufficiently complicated software is (sometimes) 
> buggy.

It's true.  Back in December 2007, I found a bug in Mizar that could be 
exploited to prove things which are quite false.  I reported the problem

through this mailing list, and it was fixed in a matter of just a few
days.
The world did not end.  Nobody was fooled into believing that there are
a 
finite number of primes.

Bill