Re: [mizar] A quote

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

Dear Piotr,

>The first major project involving a large number of people was Mizar;
>One may not agree with the above (especially in the light of the rest of the
>paper).  However, it is inevitable that people will be discouraged by the
>amount of garbage in MML.  In this light the "weak types" can wait.

I disagree.

One of my main objections to the MML is that it contains "non
empty" in places where I don't think it should be necessary.
I always thought that that was caused because of the strange
definition of "Element of".  (Correct me if I'm wrong.)

So an example where this kind of non-emptiness bit me is in
the definition of "terms".  MML contains a definition of
terms over a given signature.  This definition wasn't usable
for me because it required the set of variables to be non
empty!  And I needed closed terms!  (I was thinking of
formalizing Kruskal's theorem.)  So I gave up thinking "MML
is not very good".

(Andrzej wanted me to improve the definition of term to drop
the non-emptiness of the set of variables and then reprove
the theorems, but it never happened.)

So I realize that this is _not_ the kind of "garbage" that
the article you quoted talks of.

I think when people look at the table of contents of MML they
think "what is this SCM stuff"?  That's not the mainstream
computer science way to talk about computability.  So they
then discard MML as amateuristic.

It would be interesting to hear the opinions of professional
mathematicians about what they think is worthwhile in MML and
what is garbage.

Freek