Re: [mizar] PVS GPLed

[Jesse Alama <alama@stanford.edu>]

"Chisolm, Bill" <bill.chisolm@intel.com> writes:

> 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.

I'm not sure whether I've mentioned this before on the list, but in my
view keeping mizar's source code closed undermines one of the
philosophical goals of proof-checking, which is to make explicit as much
of the logical structure of a piece of mathematics as possible.  It's
not enough to make the full text of the MML available, nor is my point
negated by the existence of SUM, through which one can indeed get access
to the source code.  The source of the verification programs themselves
should be freely available for the mathematical knowledge formalized in
mizar to really matter (philosophically).

Jesse

-- 
Jesse Alama (alama@stanford.edu)