Certified Elm web apps

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 the extraction in the online IDE Ellie:
https://ellie-app.com/cSFtmjq99Rta1

Contributions with more interesting examples are very welcome!

1 Like