[MLton] HOL's Moscow ML implementation, and pushing MLton to emulate it

[Konrad Slind]

Hi,

   I'm a co-developer of HOL, so I hope people don't mind me
joining the discussion.

On Apr 1, 2005, at 12:16 PM, Matthew Fluet wrote:

>
> I'm confused, though part of my confusion stems from not knowing 
> exactly
> what role a value of type 'thm' plays in the HOL system.  From what
> Michael has said, I get the feeling that a 'thm' value has no 
> executable
> content, it is simply a term representation.

Exactly: a thm is  a pair (asl,c) of a list of terms (assumptions) and
a term (conclusion). There is no executable content in a theorem; it's
all data (simply typed lambda terms).

>
> Now, there is another question about what it is a term representation
> _of_.  As far as I can tell, HOL does not have a separate proof 
> checker,
> so a 'thm' is not a proof of the theorem, it is simply the statement of
> the theorem.  So, the proof of the theorem is an ephemeral object,
> implicit in the execution of the HOL REPL that constructs a 'thm' 
> object.
> There is a sort of meta-theory reasoning principle that allows one to
> conclude that having a 'thm' object is tantamount to the truthhood of 
> the
> theorem it represents.

Yes indeed. This is a neat idea due to Robin Milner:  implement a type
of theorems (thm, in HOL) and implement the primitive rules of 
inference of
the logic as functions operating on that type. Then abstract the type.
Once that is done, the only way to produce a value of type :thm is to
perform a chain of primitive inference steps. Instead of the familiar
inductive closure of a rule set, think of this as the closure of the 
rules
under ML programming. So if something of type :thm is obtained in a
HOL session, there exists a proof in the standard logician's sense. The
proof has been performed by ML evaluation, but has not been kept
(proofs are big ... the idea was invented in the mid-70s when there 
wasn't
much space in computers).

The implementation of the abstract type of theorems is often called the 
kernel
of the HOL logic ... it's our TCB!

If one was interested in keeping proofs, it's simple to instrument the
primitive inference functions in the kernel to capture the inference 
steps
for storage.

>  Now, this opens up a number of other issues about
> actually 'believing' a HOL proof.  If simply having a 'thm' object 
> lets me
> conclude that the theorem is true, then you need to worry about hacking
> the on-disk format to forge 'thm' objects that correspond to false
> statements.  If the proofs disappear, there really isn't a paper trail 
> to
> check.

True. In the 1980s we worried about these sort of things and understood
how to solve them. Having done that, the imagined "attacks" never
materialized, so we use the current scheme, and could generate
persistent proofs if an application warrants that level of paranoia.

>
> But, maybe I'm way off with the way HOL is meant to work.

No, you've definitely got the drift.

Konrad.