Re: [mizar] PVS GPLed

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

Hi Claudio,

>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?

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.

>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.)

>For these reasons I do prefer the "keep proof objects
>around" approach to the LCF style one.

I think that keeping proof objects around is orthogonal
to having a LCF style core in the first place.  In HOL
one also can keep proof objects if one likes.

So are you arguing for _not_ having an LCF style core?
Or just saying that it doesn't solve all the world's
problems?  (Something I can very much believe! :-))

Freek