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

[Stephen Weeks]

> > Yes.  The thing to keep in mind is that whatever you want to run fast
> > all has to be SML source in the same program.  In your (or your
> > users') case, that means the HOL kernel and any accompanying theory
> > code.
> 
> Right, but the point being that 'thm' values don't _run_, so you can't 
> make them any faster by including them in the SML source to be compiled.

Yep, that is definitely the point.  MLton's optimizer doesn't look too
deeply inside values of recursive datatypes.

> Dan Wang's idea of cooperating programs is probably another
> reasonable way to go.  The insight there is that there is really no
> interaction between code supporting linear arithmetic over reals and
> code supporting a list theory.  So, there isn't anything for mlton
> to exploit when it compiles the whole program.

I'm not so sure about this.  I bet that there is interaction between
the proof scripts of different theories that MLton could usefully
optimize.  That's surely some of the benefit that Joe Hurd already saw
in his experiments.

> If simply having a 'thm' object lets me conclude that the theorem is
> true, then you need to worry about hacking the on-disk format to
> forge 'thm' objects that correspond to false statements.  If the
> proofs disappear, there really isn't a paper trail to check.

I don't see how this is qualitatively different than the already
existing situation of having to defend against an adversary who
modifies the memory of a running HOL program.  If the system isn't
used according to the rules, it won't do what you want.  The on-disk
case is slightly worse because of the ease with which modification is
done and the increase in its accidental likelihood, but it's the same
problem.  It's probably worth including some checksums or whatever in
the disk files to avoid accidental mixups.