Re: PVS GPLed

On Mon, 22 Sep 2008, Freek Wiedijk wrote:

>> The same with Mizar's not exactly "wonderfully simple"
>> parser and type system. Having a "small kernel" beneath
>> them would improve my trust in Mizar, but hardly to the
>> point when I would feel safe.
>
> You could be more or less convinced that you cannot prove
> "contradiction" though, which for me is the most important
> part of trustability.
>
> Unless of course you could have a definition
>
> 	definition
> 	  pred contradiction means
> 	    ...
> 	end;
>
> somewhere :-)  So I don't think you can't, but you're right,
> you have to inspect the "parsing code" for that.  But somehow
> it seems much more trivial to make sure that _this_ cannot
> happen (I just tried it, and it seems obvious that you cannot
> do this with the current parser)

echo "R0=1" > contra.voc

environ vocabularies CONTRA; begin
definition pred 0=1 means :Def1: not contradiction; end;
theorem 0=1 by Def1;

Btw., I don't claim any originality here: some time ago I saw a seriously 
meant Mizar article with a "new functor symbol" consisting of a variable 
that is typically used for certain algebraic structure, plus some 
additional "function-looking" characters (I think brackets) around it, 
suggesting that it was some functor (brackets) applied to the variable. I 
had to look at the article in html to understand the horror (I mean: the 
infinite possibilities allowed by the Mizar parser, plus the fact that 
someone really used it this way :-).

Josef