[fmap]

I can add a few more data points. First regarding CakeML:

- CakeML is written in HOL4, which is using ML.

- SML, unlike Ocaml has a well-defined semantics and so there is a good starting point for a verified compiler.

Second, regarding Ocaml, the easiest reason for choosing Ocaml over ML is because there is only one implementation of the language that everybody is using. This makes it a lot more likely that the ocaml compiler will still be around a few decades from now. There are several modern ML compilers, most of which are more or less unmaintained. PolyML, which everybody seems to be using these days, is substantially developed by a single person.

[nickpsecurity]

On top of it, SML was literally designed to do proving. Writing provers, feeding algorithms into them, and later extracting algorithms out. Ocaml was designed as a practical language for software development. Unsurprisingly, the provers and verified tools tend to be done in SML or a subset of it while real-world software is done in Ocaml.

That said, the CakeML team welcomes a translator for Ocaml that outputs CakeML programs. Additionally, the Ocaml compiler was clean enough in architecture that Esterel was about to do source-to-object code validation required for its DO-178B-certified, code generator. They said they had to do way less work modifying or analyzing it than they expected. That means the Ocaml compiler itself might be a candidate for verification albeit probably a non-optimizing form of it. I'd also try the K framework that successfully handled the C semantics with KCC compiler. If it can handle C, I'd venture a guess that it should handle a better designed compiler and language. ;)

EDIT to add: Ocaml syntax is being worked on at link below.

https://github.com/CakeML/cakeml/tree/master/unverified/ocam...

[groovy2shoes]

> SML was literally designed to do proving.

So was Caml (and its precursor Le-ML), originally :)

That it grew so far beyond that I think is a consequence of it not having a formal definition like SML. This allows the developers to extend the language willy-nilly without going through the grueling task of extending a formal semantics. On top of that, as another commentor pointed out, is the fact that there's a single "reference implementation", which means that users don't need to worry about getting locked-in when opting to use new functionality.

That said, SML is still a fantastic base for new research projects in the PL space, mostly for the very same reasons it hasn't seen nearly as much adoption in the "practical" space as Caml: it's a small, simple, well-understood, and formally-specified language that grants researchers an excellent starting point for their inquiries and experiments.

[nickpsecurity]

Didnt know that about Caml. Neat. Perhaps a subset of Ocaml with formal semantics can do well, too.

[vkuncak]

It would be quite realistic and interesting to have a translation between the Scala subset that Leon project supports (leon.epfl.ch) and ML. A good starting point for this is Stainless, a redesigned version of Leon: https://github.com/epfl-lara/stainless