Re: [mizar] PVS GPLed

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

Hi Josef,

>Mizar is thus the last major proof assistant whose sources
>are closed, and licensing unclear.

Mizar also is one of the few major proof assistants that has
not been implemented using a functional programming language.
Mizar is a little bit different in many respects.

I was in Japan recently, visiting Nobuki Takayama, and
he told me that these licensing issues had been a reason
for him not to put Mizar on his KNOPPIX/Math DVD (see
<http://www.knoppix-math.org/>; it's a DVD with all kinds
of mathematical software packages that you can boot from
and then everything will just work.)

He told me that with a special arrangement it still could
be on the DVD after all, and that he might contact the Mizar
group about it.  But then it won't be on the version that you
can download (because that only can have "free" software),
but just on the physical disks that have been burned.

Personally I don't care so much for Mizar being open source.
I won't understand the sources anyway :-)  (I do sometimes
wonder whether if I dug into the sources, I could give
Mizar empty types.  But I guess not.)

Freek