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