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

[Daniel C. Wang]

Matthew Fluet wrote:
{stuff deleted}
> But, maybe I'm way off with the way HOL is meant to work.

I think the confusion is what is on disk are "proof scripts" along with the 
statement of the thm proved. i.e. a sequence of ML functions that are 
applied in some order, such that if the functions don't raise an exception 
you can be confident that the resulting thm object constructed is true.

Because of that what's stored on disk has some computational component that 
needs to get executed.