Re: PVS GPLed

Hi Freek,

On Fri, 12 Sep 2008, Freek Wiedijk wrote:

>> Mizar is thus the last major proof assistant whose sources
>> are closed, and licensing unclear.
>
> 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.)

The same e.g. with David Wheeler's listing: 
http://www.dwheeler.com/essays/high-assurance-floss.html#theoremprovers . 
Non-FLOSS software is plainly ignored.

Josef