[MLton] Implementing HOL in MLton (forwarded from Scott Owens)

[Michael Norrish]

I received the following comment from Scott Owens, who was happy for
me to forward it to the list.

Michael.

----------------------------------------------------------------------

I was perusing the MLton mailing list archives, for reasons unrelated
to HOL, and came upon your message about moving HOL away from Moscow
ML to MLton.  An idea sprang to my mind, and I can't resist sharing
it.  I haven't given much thought to its practicality, but I think
it's elegant from a language person's viewpoint.

1) Implement an SML interpreter in SML, compile the interpreter to an
   executable with MLton and run HOL on the interpreter.  Of course,
   this is likely to be even slower than using the Moscow ML
   interpreter to run HOL.

2) Augment the SML language supported by the interpreter with core HOL
   constructs (the kernel, METIS_TAC, and so on).  Now the core of HOL
   is running at compiled and not interpreted speeds.  This shouldn't
   be too hard since HOL and the interpreter are both written in SML.
   It should just be a matter of including the relevant parts of HOL
   in the interpreters source and having the interpreter offer the
   appropriate HOL types and functions as primitives to the programs
   it interprets.

3) Add a bootstrapping mechanism that allows other SML proof
   procedures and already-proven theory files to be moved from the
   interpreted world into the interpreter itself.

I suspect some of the MLton or another existing SML compiler could be
re-used in writing the interpreter.

----------------------------------------------------------------------