Dear Coq community,
I would like to share a project related to the Elm functional programming language.
As part of ConCert (https://github.com/AU-COBRA/ConCert), we have developed an extraction pipeline that allows for generating Elm code.
We have several simple examples/tests here https://github.com/AU-COBRA/ConCert/blob/master/extraction/examples/ElmExtractExamples.v.
A more "domain-specific" example with a web-app consisting of an input form, validation and rendering a list of users is available here:
The example is inspired by a similar one from the Elm guide.
We use Coq's subset types to encode the invariants for the part of the model that represents valid data.
Currently, we write the "logic" of the app (model and validation) in Coq, extract it and then concatenate with the hand-written view, that renders the form and calls the model functions.
Here is the result of extraction in the online IDE Ellie:
(the form validation rules: non-empty name, password length >= 8, passwords in the two fields must be the same).
Contributions with more interesting examples are very welcome!
That does look like an interesting project to me, as I am interested in formal verification of web applications. I am wondering how you can deal with the type system of Elm which is very strict, by opposition of OCaml which allows
Obj.magic. But I guess I should read more about the project
Other quick questions / thoughts:
I am working on https://github.com/clarus/coq-of-ocaml where I have troubles supporting all the features of OCaml, and sometimes dream of having a simpler input language. Somehow Elm seems to be exactly that, but I was kind of afraid of the small size of the community.
If you compare it to the community using OCaml to build webapps, I'm not convinced it is that small.
Ah OK, I remember you liked Elm!
I looked at it again a few weeks ago, and this is the post which frightened me: https://www.reddit.com/r/programming/comments/fxvlow/why_im_leaving_elm/
maybe haters gonna hate
I am wondering how you can deal with the type system of Elm which is very strict, by opposition of OCaml which allows Obj.magic. But I guess I should read more about the project
Hi @Guillaume Claret , that's a very good question :) Basically (as many our target), Elm does not support unsafe coercions of types. Therefore, one could end up with something that does not type check. On the practical side, in most cases polymorphism + subset types (Coq's
sig) is sufficient for many purposes. We also provide a way to inline and specialise (a bit) certain definitions, so as a result, the extraction produces well-typed code.
OK, cool to see that this is possible
(avoiding unsafe coercions)
I think it would be interesting to go the other direction also, Elm -> Coq, as the Elm language is designed to be small and strict, so that the translation may be possible in a systematic and clean way
We explored a similar direction before extraction: https://github.com/AU-COBRA/ConCert/tree/master/embedding
lambda-smart is a pure subset of System F-based language.
You can find more details here: https://arxiv.org/abs/1907.10674
OK thanks! (Bas Spitters told me about this approach for smart-contracts)
OK, cool to see that this is possible
Of course, in our development, we looked mostly at smart contracts, but we used the same extraction to extract some programs from CertiCoq benchmarks, that use Coq's
FSet. After some pre-processing it worked.
(the target language was Rust, but we haven't use unsafe features)
Of course, one always can craft an example that extracts to something ill-typed :) But I hope many things one interested in for web development could and extracted to well-typed code. Rank-2 polymorphism sometimes gets in the way, for now, we solved it with inlining/specialising.
Last updated: Jun 01 2023 at 12:01 UTC