[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] Private DB
Hi Freek,
On Mon, 25 Sep 2006, Freek Wiedijk wrote:
(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?
Sure, me :-).
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.
And now you are infected, and whatever formal math program you'll write,
they'll sue Herman :-).
So PVS is one of the most used proof assistants for computer
science applications, right?
I would not say that for mathematics.
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.
At least, PVS is documented. At least, you know its licence.
Also, software/hardware verification is much closer to business, and it is
more understandable that people think about distribution of whatever
profit there can be. The comparison I prefer is between MathWorld and
Wikipedia/PlanetMath. Why should I submit anything to the privately owned
MathWorld with their various restrictions, when I can do the same with
wikipedia, and use everything there without restrictions? So _I_ am
definitely scared away from MathWorld.
Josef