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

[Stephen Weeks]

> I would have thought that the reason that they didn't want this sort
> of approach is that in addition to having the _code_ for every
> theory in the executable, this would require the _data_ for every
> theory resident in the heap at all times.

That would hurt.  Maybe it could be avoided by loading dummy libraries
with trivial theorems (of negligible size) for those theories that
will be unused.  But that definitely doesn't support dynamic loading
of theories, and so one will need all the theories in an executable
that exposes an interpreter.