Re: [mizar] PVS GPLed

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

Bob:

>Hmmm.  I've heard everything is related.

You might be right about that.  I've heard that in fact
"(A implies B) or (B implies A)" is a tautology.

>I was having a daytime nightmare about a possible world
>in which some versions of a hypothetically liberated
>Mizar reported that something was a theorem while
>others said that it was not.

I now see the connection, thanks for the clarification.

For a system that uses the LCF architecture this risk seems
negligible.  Maybe it's time for an open source Mizar clone
-- compatible with the MML of course! -- that uses the LCF
architecture? :-)

>It seems that even checking alleged theorems about concrete
>bignum arithmetic is getting increasingly harder.

Only if you want them to be proved at GMP speeds.

Maybe someone should prove GMP correct, and then compile
it using Xavier Leroy's Compcert compiler? :-)

Freek