I've been wanting to ask one of you about certified compilation for Ocaml. SML has FLINT and CakeML. I know Leroy et al were working on a Mini-ML compiler. Are there any results yet on a certifying compiler for Ocaml, though? Anyone made a lot of progress? Or can it be converted to equivalent ML that can go through something like CakeML?
Last high-assurance work I saw done with Ocaml was Esterel's SCADE generator, which certified object code by hand. They praised the compiler for how much work they avoided w/ minimal mods. They conceivably could've gotten more done if that was automated, though.