Danil Annenkov (Apr 12 2021 at 13:20): Danil Annenkov (Apr 12 2021 at 13:20):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:
https://github.com/AU-COBRA/ConCert/blob/master/extraction/examples/ElmForms.v
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:
https://ellie-app.com/cSFtmjq99Rta1
(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!
Guillaume Claret (Apr 12 2021 at 13:29):Hello,
Guillaume Claret (Apr 12 2021 at 13:31):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
Guillaume Claret (Apr 12 2021 at 13:33):Other quick questions / thoughts:
Guillaume Claret (Apr 12 2021 at 13:35):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.
Théo Zimmermann (Apr 12 2021 at 13:37):If you compare it to the community using OCaml to build webapps, I'm not convinced it is that small.
Guillaume Claret (Apr 12 2021 at 13:37):Ah OK, I remember you liked Elm!
Guillaume Claret (Apr 12 2021 at 13:37):OK
Guillaume Claret (Apr 12 2021 at 13:40):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/
Guillaume Claret (Apr 12 2021 at 13:40):maybe haters gonna hate
Danil Annenkov (Apr 12 2021 at 13:41):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.
Guillaume Claret (Apr 12 2021 at 13:42):OK, cool to see that this is possible
Guillaume Claret (Apr 12 2021 at 13:43):(avoiding unsafe coercions)
Danil Annenkov (Apr 12 2021 at 13:44):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
Guillaume Claret (Apr 12 2021 at 13:48):OK thanks! (Bas Spitters told me about this approach for smart-contracts)
Danil Annenkov (Apr 12 2021 at 13:48):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 FMap and FSet. After some pre-processing it worked.
(the target language was Rust, but we haven't use unsafe features)
Danil Annenkov (Apr 12 2021 at 13:52):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: Oct 12 2024 at 13:01 UTC