[MLton] Isabelle on MLton?

[Stephen Weeks]

> > what would MLton have to offer over the other compilers that already do
> > that?
> 
> Stability? 64 bits? Moderate memory consumption?

All goods points (64 bits in the future for MLton but coming).
Although at least the latter also partially benefits from
whole-program optimization.

> However, we'll also take a closer look to see if the many "use"s can
> be eliminated. It won't be easy and it would make the system less
> (easily) user-extensible.

Perhaps this will lead to a useful middle ground that can be had using
existing systems' capabilities (i.e. Poly/ML's REPL and MLton's
performance).  Namely, develop with Poly/ML and use its REPL for
interactive proof development and user extensibility.  Then, when
you've got the "whole" proof and need to do a long computation, feed
everything to MLton for improved performance.