Re: PVS GPLed

Hi,

I cannot resist stepping in since I also think that the claims about
systems with small kernels are a bit over-rated. But for different
reasons.

It is NOT possible to override/overload the thm type in any serious way.

On the other hand, I do not agree with Freek that the
parsing/pretty-printing layer is too simple to hide what is really going
on. The small kernel just tells you that there is a proof for the output
of the parsing level and can show you the pretty-printed form. But the
parsed statement can be quite different from what you had in mind. And,
if you also mind your proof and not only the existence of one proof, the
proof that was built usually _is_ much different from what you had in
mind. I.e. the parsing/pretty-printing level is usually quite thin for
formulae, but very thick for proof steps.

One counter-claim is that the type of what you proved can be
pretty-printed back to be checked. And, since the pretty-printed version
must look like your input, the parsed form cannot be too dummy (e.g.
True). However, this is not always the case. For instance, in Coq some
information about the user syntax is kept in order to pretty-print it
back exactly as the user typed it. In other words, the system is
"cheating" by skipping the parsing/pretty-printing cycle for some
formulae. Skipping this cycle can potentially hide some weird
translation.

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

						Cheers,
						C.S.C.

-- 
----------------------------------------------------------------
Real name: Claudio Sacerdoti Coen
Doctor in Computer Science, University of Bologna
E-mail: [email protected]
http://www.cs.unibo.it/~sacerdot
----------------------------------------------------------------