Re: [mizar] MML License

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

Hi Josef,

>Theorema provides neither binary nor source.

It doesn't!  I hadn't realized that.  (Maybe there is no
"binary", Theorema is just a bunch of Mathematica scripts...
I think.)

>"PVS being the most popular assistant" seems a bit strong
>assertion, could you explain why you think so?

That was the impression I got at TPHOLs.  It might be
interesting to match talks to systems at the next one.

And I meant, "most popular for the thing that proof
assistants are mostly used for", which is verification of
circuits and protocols and programs and so on.

>Do you think that could be strengthened to "the most popular
>assistant for writing formalized math"?

Certainly not!  I don't know which system is the most popular
for that (in terms of number of people who currently are
actively using the system to do formalizations).  I would
find it hard to decide between Mizar, Isabelle and Coq.  (Or
does anyone think it's still another system?)

Freek