Re: [mizar] PVS GPLed

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

Bill:

>I, for one, would look at the source code if it were
>available.

But would it help?  Understanding Mizar's behavior by
experimenting around with it to me seems much easier than
understanding it by looking at the implementation.  We're not
talking about an relatively abstract language like ML or
Haskell here, so the implementation is rather low level.

>As one example, I would like to understand the rules that
>Mizar uses for parsing a Term-Expression.

Really?  I've had many frustrations with Mizar (still have),
but this one I have never found confusing.

My problem generally is not that I don't understand how
Mizar parses a term, but mostly that I often am mystified
by the way it resolves the overloading.

>The correct parse tree can actually be *changed* by adding
>or removing functor definitions.

No.  The parse tree will be the same.  The interpretation of
the symbols will change, but the parse tree will be the same.

>If the world were perfect, then these things would all
>be neatly written in a well-organized reference manual.
>However, that manual may never be completed in our real
>world.

I once started such a manual.  My "tutorial" ("... in nine
easy steps") was supposed to be part of it.  But no one in
the Mizar group seemed to think it would be useful (which I
still find very strange!), and by now I don't think I ever
will write it.  Not as long as Mizar doesn't support empty
types, doesn't have much simpler environments, doesn't have
binders, doesn't have the old style "from" :-)  Ah yes:
and doesn't support "then" after "consider".

Freek