While it's not as robust as static-typing, compile-time type checking for Erlang has come a long way. Eqwalizer works pretty well, though but I may be biased since my employer sponsors the project.

1. https://github.com/WhatsApp/eqwalizer

You've been able to write PureScript compiled to Erlang for years. PureScript is a well tested language at this point, and the Erlang compilation works very well. Statically typed message passing is a non-issue in practice and it has been a bad reason for not having it the whole time.

I've been using Elixir since 2015 and can confidently say there is no use case I would choose Elixir for over PureScript for the BEAM. In practice my projects are Elixir + PureScript because we can have them interoperate, but there are zero technical reasons to choose Elixir over PureScript for BEAM work.

Edit:

`dialyzer` and similar tools are unusable for almost all sizes of projects in part because they're badly made, they're too lax and have zero useful abstraction properties. Making a spec generic, for example, is an exercise in futility, whereas an actual type system has no issues with expressing that very basic property.

I'd like to see someone tackle a PhD thesis (or ten) on applying formalism to the concept of migrations. I suspect there's a missing aspect of type/group/category theory that's at least as big and important as variance is.

I think it might already mostly exist, it just isn't organized into a discipline.