[madsbuch]

Well, as with all logic systems you can only express correctness up to its granularity. Elm's type system is, as you mention, very rudimentary and basically just HM + reactive programming.

First, I don't write any serious applications in Elm, and would never do it. I don't find that it is productive because of the reasons you list. Just as I would never write any serious applications in Coq.

But with Elm, as with Coq, I can appreciate that their goals are not immediate developer productivity. Maybe some day when the ecosystems needed are fully implemented. Until then I just applaud everybody working on systems that are strongly typed and ensure that all their dependencies are.

I believe this will provide tremendous value – when ripe.