|
|
|
|
|
|
by nickpsecurity
3463 days ago
|
|
|
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... |
|
|
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.