Re: [mizar] Private DB

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

Hi Josef,

>(as a member of SUM)

I haven't paid my contribution in years...  I always have the
problem that I don't know (a) how much it is and (b) where I
should send it.  Are there other SUM members with the same
problem?

>And that's also why I have advised Jesse Alama who had the
>good intent to package Mizar for the Fink packaging system to
>first ask about it here, because the legal situation is
>really unclear. It's really quite a bit of pain today.

I wouldn't mind having Mizar be "free software", but then I'm
not the one who wrote it!  It _would_ be nice to have a Debian
package for Mizar, yes.

>And yes, you shouldn't be required to be a member of any
>organisation to do research in formal math.

I don't feel too strongly about this.  PVS is very much
non-free too.  I once tried to get a license from SRI to be
able to see some PVS related source code.  It was almost
impossible (it took me more than a year, I think)!  They
wanted to be able to _sue_ when something bad happened to
their code, and I was not sueable enough.  So when I sent them
my signed form (faxing was not good enough), they refused it.
They wanted the signature from an important person from my
university.  Luckily Herman was important enough for them.

So PVS is one of the most used proof assistants for computer
science applications, right?  So apparently this behavior
hasn't scared away people in the way that some people might
think Mizar is scaring away people by not having their source
code open on the web.

Freek