[MLton] HOL's Moscow ML implementation, and pushing MLton to
Daniel C. Wang
Fri, 01 Apr 2005 15:09:46 -0500
Matthew Fluet wrote:
> 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.