[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] PVS GPLed



On Mon, 22 Sep 2008, Freek Wiedijk wrote:


I.e. the parsing/pretty-printing level is usually quite
thin for formulae, but very thick for proof steps.


Sorry, but I don't understand this.  What do you mean with
"proof steps" here?

In Mizar proof steps basically _are_ formulae, so how can
the meaninig of formulae have "thin" parsing, while the
parsing of proof steps is very thick?
It is generally more "thick" to "understand" a proof step, i.e. to understand how the system verified it - I don't know if this is what Claudio includes into "proof step parsing". Even in Mizar this can be pretty hard, and certainly with systems that have ASM_MESON, Metis, or Zenon. 


Also, I think that mathematics is "proof irrelevant".
Once you prove something, it doesn't matter whether you know
what the proof is to know that it's provable.  So even if
you can be misguided about the proof steps, you wouldn't
believe false statements.
I agree quite a lot, OTOH there are cases where knowing the proof makes significant difference - e.g. Bob Solovay's recent analysis of the proof of CARD_LAR:37 lead to (for me surprising) conclusion that the "common" ZFC definition of "strongly inaccessible cardinal" is bad in Tarski-Grothendieck for certain purposes. I think that the experience with both human fallibility and computer systems' fallibility shows that it is good to have some ideas about how the proofs proceed. 


For instance, in Coq some information about the user syntax
is kept [...]


So when I wrote this I was thinking about HOL, where formulae
syntax is wonderfully simple.  In Coq with all the coercions
things are worse, I agree.  (I think that Herman at some
point used coercions in Coq to prove a theorem that looked
like 0 = 1.  Or he made 0 = 1 look like 0 = 0, I forget.)
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. So I really think that the argument for safety of HOL Light is not just "small kernel", but an overall code inspection (involving more than the 669 kernel lines). 

Josef