Re: [mizar] PVS GPLed

["Chisolm, Bill" <bill.chisolm@intel.com>]

Josef Urban wrote:
> Mizar is thus the last major proof assistant whose sources are closed,
> and licensing unclear.

Freek Wiedijk wrote:
> Personally I don't care so much for Mizar being open source.
> I won't understand the sources anyway :-)

I, for one, would look at the source code if it were available.  There 
seems to be a lot of essential information about Mizar that is not 
written down anywhere.  I have learned some of that unwritten knowledge 
by reading the mailing list, and by asking people.  I have learned even 
more of it by doing experiments with Mizar.  But I still have questions
about Mizar that I can't answer.  If the source code were available, I 
would look there for an answer whenever Mizar does something that I 
just don't understand.

As one example, I would like to understand the rules that Mizar uses 
for parsing a Term-Expression.  This is not just a theoretical question 
about the Mizar language.  It is a practical question, because anyone 
who reads the MML will encounter many, many expressions whose correct 
structure is hard to recognize.  How can a human reader predict which 
way Mizar will parse an expression?

It's not enough just to just consult the Mizar grammar on the web:
  _http://www.mizar.org/language/pages/term-expression.html
That grammar is ambiguous.  It allows multiple different ways of 
parsing any particular expression.  The grammar does not tell us how 
to apply the precedence levels that are specified in the mml.vct file. 
It also does not tell us that there is even more background information 
which is needed to parse an expression correctly.  The parser also must 
know how many left and right operands each functor can accept, 
under each functor definition that is available to the article. 
The correct parse tree can actually be *changed* by adding or removing 
functor definitions.  As a new user, I had to learn these unexpected 
facts by trial and error.

This kind of information about Mizar is just not written anywhere, but 
a person must know these things in order to be successful at writing 
Mizar articles.  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.

Opening up the source code will not be a substitute for the 
comprehensive manual that has never been written.  But it will enable 
some Mizar users to independently find answers to some of their 
questions.  I am one user who would find that very helpful.

Bill Chisolm