Ana de Almeida Borges (Oct 13 2021 at 10:25): Ana de Almeida Borges (Oct 13 2021 at 10:25):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.
Yannick Forster (Oct 13 2021 at 10:33):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
Bas Spitters (Oct 13 2021 at 10:56):Not to ocaml yet, but we have a general framework for verified extraction to ML-like languages.
https://github.com/AU-COBRA/ConCert
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...
Ana de Almeida Borges (Oct 13 2021 at 11:41):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 => to -> 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".
Ana de Almeida Borges (Oct 13 2021 at 11:44):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?
Bas Spitters (Oct 13 2021 at 18:33):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.
Karl Palmskog (Oct 13 2021 at 18:37):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
Karl Palmskog (Oct 13 2021 at 18:37):it's not like the OCaml compiler is going to be verified anytime soon, even if the OCaml program source is verified...
Last updated: Oct 13 2024 at 01:02 UTC