Re: PVS GPLed

On Fri, 12 Sep 2008, Piotr Rudnicki wrote:

> On Fri, Sep 12, 2008 at 11:57:23AM -0700, Chisolm, Bill wrote:
>
>> 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?
>
> In such case I consult Josef's xml version of MML which answers all such
> questions (OK, modulo weird links at times).

But having available the correct parse of a term only answers one 
question, it may still be difficult to guess the algorithms. And it is - I 
tried quite hard to reverse-engineer the various algorithms before I had 
Mizar sources, and never got it right. Others have tried and failed too. 
Exercise in futility, stealing precious time of the (relatively few) 
people who wanted to do some work with Mizar, and further decimating their 
numbers.

> While I am not planning to study Mizar sources, I am strongly in favour that
> the authors make the sources open.  I can understand that the authors may be
> ashamed of their coding but if the sources are open then some energetic
> volunteers will clean the code pretty soon (and preserve the semantics too).

And possibly even document Mizar :-). I never heard a serious explanation 
of why the sources are closed, and as far as I know there was never a 
serious rational discussion about it. I really would like to know the 
reasons, and have a serious discussion about this. One thing I hear quite 
often is that Mizar is badly documented, because the developer team is 
small. Guess why?

Josef