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

[Daniel C. Wang]

I haven't looked to closely at the HOL4 infrastructure in a while, but I 
suspect that most of these theories don't share any state. If that's the 
case you could develop an architecture where various different MLton process 
communicate via RPC/IPC. This can avoid the need to build one big monolithic 
system. If the RPC/IPC becomes a performance bottleneck, you take the 
appropiate modules you need and build the monolith you want, but otherwise 
you can do quick experiments by just recompling the theory you are hacking 
on. (Also, if you're clever you can take advantage of a dual processor or a 
cluster to do distributed theorem proving!)

Stephen Weeks wrote:
>>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.
>