I&#x27;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?<p>Last high-assurance work I saw done with Ocaml was Esterel&#x27;s SCADE generator, which certified object code by hand. They praised the compiler for how much work they avoided w&#x2F; minimal mods. They conceivably could&#x27;ve gotten more done if that was automated, though.