[nickpsecurity]

Everyone with formal method background interested in this work should consider taking on one of their posted projects that would improve it. Especially Ocaml to CakeML translator.

https://cakeml.org/projects

Just email them first in case someone has done the work already. Academics sometimes are slow to update web sites due to digging deep into their research. ;) The best uses I can think of for CakeML are:

A reference implementation to do equivalence checks against with main language, a ML or not, being something optimized.

Someone to build other tools in that need high assurance of correctness. Prototype it to get the algorithm right using any amount of brains and tooling that already exist with an equivalent CakeML program coming out. Then, that turns into vetted object code.

A nice language for writing low-level interpreters, assemblers, or compilers that bootstrap others in a high-confidence way. Idea being in verifiable or reproducible builds where you want a starting point that can be verified by eye. They can look at the CakeML & assembly output with some extra assurance on top of hand-doing it. One might even use the incremental compilation paper on building up a Scheme to end up with a powerful, starting language plus assurance binary matches code.