Re: [mizar] PVS GPLed

[Makarius <makarius@sketis.net>]

On Tue, 16 Sep 2008, Freek Wiedijk wrote:

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

Abstract types are fine if you really stay within ML world, and have a 
waterproof implementation of the ML compiler/runtime.  I have been told 
that OCaml is not fully type-safe in that respect due to "object magic" 
features.  SML as a general language definition is a bit better, but 
particular implementations also provide "magic" entries that can mess up 
datatype integrity.  Other sources of uncertaincy are separate compilation 
(OCaml) or persistent heap images (Poly/ML).

So your assumptions are that the overall system architecture is able to 
keep the critical parts of the implementation somehow local.  The LCF 
inference kernel may stand as a representative for that principle.


	Makarius