3 ms·
> nothing more solid than "Coming Soon(tm)". That's untrue. There's way more out there than 'coming soon'. There's a repo with code, talks at the OCaml Worksho
by amirmc 11y ago
> nothing more solid than "Coming Soon(tm)".
That's untrue. There's way more out there than 'coming soon'. There's a repo with code, talks at the OCaml Workshop and blog posts describing it.
This isn't the kind of project where you want to 'move fast and break things'.
- nickpsecurity 11y agoI'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.