Danil Annenkov, Mikkel Milo, Bas Spitters (ML’21 at ICFP’21)
Abstract: The Coq code extraction feature produces executable code in conventional functional languages that can be integrated with existing components. Currently, Coq features extraction into OCaml, Haskell and Scheme. Many new target languages are not covered by the standard Coq extraction, such as languages for smart contracts and web development. Moreover, the extraction procedure is written in OCaml and is not verified. Implementing extraction in Coq itself allows for verification of the extraction process. We implement an extraction pipeline by extending the MetaCoq verified erasure with proof-generating passes and verified optimisations. We support several languages from the ML family in our pipeline: two languages for smart contracts (Liquidity and CameLIGO) and the Elm programming language. Our experience shows the pipeline can handle practical use cases and can be extended with more target languages including the ML family.
Any comments, suggestions, questions would be welcome.
I do research mathematics as a hobby. I became aware of Coq because of its use in Voevodsky’s Univalent Foundations of mathematics, and its capabilities for formalising proof.
It’s pleasant to see a connection between this and Elm.
This looks really neat! Thank you for sharing! I have some questions:
would it be interesting to try and generate more idiomatic code? For example, the generated Elm code defines a model using a custom type constructor instead of a record. It also defines existsb : (a -> Bool) -> List a -> Bool, which appears to duplicate elm/core's List.any (but maybe this was required for Coq to check it?)
do the limitations (especially on tail-recursion) you list for Liquidity and CameLIGO apply to the Elm extraction as well?
do you plan to productionalize the code extrator you’ve written? (e.g. make it available on the Coq package index?)
Yes, we’re working on better support for records in general.
It’s easy to remap existsb to list.any. In general, the list of remappings is extensible.
(However, each remapping will increase the trusted code base, as that translation is not verified.)
I expect things to work much nicer in elm, as the language is much closer to the one of Coq.
Part of my group is currently on holiday, but we’ll come back with a more detailed answer.
We provide an opam package. We may move it to a more central place at some point.
@spitters already gave good answers, I’ll just clarify some of the points.
Records: it’s possible to add syntax for records. One reason we didn’t do it, is because the pretty-printer has to be trusted and without special support for records, the code is simpler. But there are no conceptual problems with printing records, in fact, users can tweak the printing procedure, if necessary.
Using more Elm standard functions: this is totally up to the user to decide what corresponds to Elm stdlib (or other libraries).
Here is a translation table for the web app: ConCert/ElmForms.v at master · AU-COBRA/ConCert · GitHub
Limitations: basically none of the Liquidity and CameLIGO limitations apply to Elm. The only one is the absence of unsafe type-casts, but our experience shows that if one remains in Hindley-Milner subset of Coq, plus subset types (like a type of positive numbers, non-empty lists and other types with constraints), our extraction produces well-typed Elm code. Using higher-rank polymorphism is also possible, our inlining machinery allows for unfolding and specialising such definitions in many cases (like using monads defined as a type class in Coq). Therefore, it’s possible to leverage the expressiveness of Coq and still produce well-typed Elm code.
Some examples of using recursion: https://ellie-app.com/dKwDPB2SDLza1
As @spitters said, we have an opam package config that can be used to install ConCert as a dependency.
I really encourage everyone to contribute with more Elm examples, so we can see together how our current development can be improved.
Just fork it, build and start experimenting
