Re: [mizar] PVS GPLed

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

Josef:

>I like the "small kernel" approach of HOL Light (or was it already LCF?), 

Yes, LCF already I think.

>and think that it is really very useful and "trust-encouraging". But I 
>think it still requires quite some trust, assumptions, and knowledge about 
>the implementation, when you say that thousands of additional lines of 
>code "are safe" provided the small kernel is.

Why?  When in HOL I have an object of ML type "thm", I _know_
that the statement of that theorem will be provable in the
HOL logic.  (Provided that there are no bugs in the kernel,
of course.)  It's the power of abstract datatypes.  So what
are the assumptions and knowledge of the implementation
that you're referring to?

Of course the definitions of your mathematical notions might
not mean what you think they mean, and the prettyprinter
might show statements in a misleading way.  But still what
it actually _is_ will be mathematically correct.

But in the practice of HOL definitions generally are quite
clear and simple, and the prettyprinter generally doesn't
confuse you.

So is there anything else that you have in mind when
you write "... assumptions, and knowledge about the
implementation"?

Freek