Re: 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