MLton is unsuitable for LCF-style theorem provers, simply because it has no interactive toplevel.
ML was originally developed as a MetaLanguage for such theorem provers. The idea is to have an abstract type thm of theorems, whose operations (like modus ponens) only allow you to construct provable theorems. To prove a theorem interactively, you would start the ML toplevel and try to construct a proof of your proposition by programming in ML. The ML type system guarantees that you can only prove valid things. The toplevel is essential if you want to prove things interactively.
Modern theorem provers like Coq work differently. If Coq were written in SML rather than OCaml, then MLton should be good for Coq as well. I think people have experimented with non-interactive versions of HOL4, compiled using MLton (because it's faster than other SML compilers).
LCF-style provers do not use the Curry-Howard correspondance (ML's type system is not strong enough); having something of type thm is not enough to know that it's a theorem. The type thm is just a triple of tag (to store any oracles etc), a list of assumptions and a conclusion. The main way that you prevent against fake theorems being constructed is to (I think) make the constructor private, and then have combinator functions that you've very carefully verified. You can certainly use mk_thm to make a theorem of whatever you want (it adds an oracle tag, but a single line change in Thm.sml would drop that).
MLton would require you to write your own metalanguage (but this is not necessarily onerous; most Isabelle is written in thy files or Isar.
I had a think about it, and I think that the actual compelling advantage of Poly is probably its saveable heaps; they really make everything a lot faster.
The whole language is a bit janky though; there's a tonne of stuff totally unstandardized (production of executables, imports etc), which means that every compiler has fairly dramatic extensions (and hilariously you can't tell between them by attempting to use them because of the type system).
So HOL4 will try to determine whether you're using mosml or polyml by calculating factorial 100. With mosml you overflow, polyml seamlessly switches to a bignum.
tl;dr Coq implements a metalanguage on top of ML (with an undecidable type system). LCF type provers use ML as their metalanguage. Using mlton would force you to write your own metalanguage because it has no interactivity.
> The main way that you prevent against fake theorems being constructed is to (I think) make the constructor private, and then have combinator functions that you've very carefully verified.
That's what I mean. The LCF approach is to give you a signature with an abstract type thm and operations to construct its inhabitants. The operations are such that you can only construct valid theorems. Example (taken from http://www.cl.cam.ac.uk/~jrh13/slides/sri-20feb05/deduction....):
module type Proofsystem =
sig type thm
val axiom_addimp : formula -> formula -> thm
val axiom_distribimp : formula -> formula -> formula -> thm
val axiom_doubleneg : formula -> thm
val axiom_allimp : string -> formula -> formula -> thm
val axiom_impall : string -> formula -> thm
val axiom_existseq : string -> term -> thm
val axiom_eqrefl : term -> thm
val axiom_funcong : string -> term list -> term list -> thm
val axiom_predcong : string -> term list -> term list -> thm
val axiom_iffimp1 : formula -> formula -> thm
val axiom_iffimp2 : formula -> formula -> thm
val axiom_impiff : formula -> formula -> thm
val axiom_true : thm
val axiom_not : formula -> thm
val axiom_or : formula -> formula -> thm
val axiom_and : formula -> formula -> thm
val axiom_exists : string -> formula -> thm
val modusponens : thm -> thm -> thm
val gen : string -> thm -> thm
val concl : thm -> formula
end;;
With this type signature, the ML type system guarantees that only valid theorems can be constructed. Note that this is not Curry-Howard. Of course, you can punch holes into this by allowing unproved assumptions using mk_thm or the like. But the original idea was to implement all other tactics only using such a correct-by-design structure.
ML was originally developed as a MetaLanguage for such theorem provers. The idea is to have an abstract type thm of theorems, whose operations (like modus ponens) only allow you to construct provable theorems. To prove a theorem interactively, you would start the ML toplevel and try to construct a proof of your proposition by programming in ML. The ML type system guarantees that you can only prove valid things. The toplevel is essential if you want to prove things interactively.
Modern theorem provers like Coq work differently. If Coq were written in SML rather than OCaml, then MLton should be good for Coq as well. I think people have experimented with non-interactive versions of HOL4, compiled using MLton (because it's faster than other SML compilers).