Stream: Miscellaneous

Topic: Certified Elm web-apps


view this post on Zulip 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!

view this post on Zulip Guillaume Claret (Apr 12 2021 at 13:29):

Hello,

view this post on Zulip 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

view this post on Zulip Guillaume Claret (Apr 12 2021 at 13:33):

Other quick questions / thoughts:

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Guillaume Claret (Apr 12 2021 at 13:37):

Ah OK, I remember you liked Elm!

view this post on Zulip Guillaume Claret (Apr 12 2021 at 13:37):

OK

view this post on Zulip 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/

view this post on Zulip Guillaume Claret (Apr 12 2021 at 13:40):

maybe haters gonna hate

view this post on Zulip 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.

view this post on Zulip Guillaume Claret (Apr 12 2021 at 13:42):

OK, cool to see that this is possible

view this post on Zulip Guillaume Claret (Apr 12 2021 at 13:43):

(avoiding unsafe coercions)

view this post on Zulip 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

view this post on Zulip Guillaume Claret (Apr 12 2021 at 13:48):

OK thanks! (Bas Spitters told me about this approach for smart-contracts)

view this post on Zulip 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)

view this post on Zulip 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: Aug 14 2022 at 13:02 UTC