Re: PVS GPLed

On Tue, 16 Sep 2008, Freek Wiedijk wrote:

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

You e.g. "know or assume" that there are no ways how to shadow the "ML 
type thm" in the rest of code, and in case there are some ways, you know 
the implementation enough to say that they are not used. I know neither 
the various ML dialects, nor their parsers/preprocessors, nor the 
implementation. Maybe my concern can be trivially dismissed by more
knowledgable people, but I'd have to trust them :-).

Josef