Some time ago there was an open call for a PhD student to work in Nantes on certified OCaml extraction. It has not been enough time to finish a PhD, but I wonder: has there been any progress on this goal, and is there some public repository about it? I mostly wanted to know whether there was / would soon be some prototype that could be tried.
Hey Ana! First: it's cool that your interested in this :) There is no code yet, but at least pretty concrete plan by now. That means it's too early to try a prototype unfortunately :/ But would you be willing to explain what your use case would be? That might help us in ensuring that a first prototype (which might be partial in functionality) can actually be tried on your examples
Not to ocaml yet, but we have a general framework for verified extraction to ML-like languages.
We'll be collaborating with the metacoq team on this.
There is also a Why3 related effort of verifying ocaml. I forgot the name though...
Hi Yannick, of course! The use case would be extracting fairly simply Coq functions, which were written in an attempt to mimic the OCaml syntax as much as possible, and such that the extraction could in principle be as simple as changing
-> and so on. It doesn't have any dependent types, for example. Right now the extracted code is very readable and has no
Obj.magic. We do map some Coq types to OCaml types, but otherwise I don't think we use any fancy features. As for the reasons, well, it boils down to "more verification is better".
Thanks for the pointers Bas! Does the "yet" in "not to ocaml yet" mean that something is indeed in the works? Or that it would be easy to adapt?
Not "yet", in that we aim to collaborate with Yannick.
If the code really is as simple as you describe it might we worth trying to adopt the elm printer we have in concert to ocaml.
has anyone considered the option of getting the CakeML semantics into Coq and doing what they did here for Isabelle: https://lars.hupel.info/pub/isabelle-cakeml.pdf
it's not like the OCaml compiler is going to be verified anytime soon, even if the OCaml program source is verified...
Last updated: Feb 09 2023 at 03:06 UTC