Re: [mizar] PVS GPLed

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

Hi Josef,

>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) than to have to trust a
rather big system that does a lot of complicated things.

Freek