Elixir with static typing would be an absolute dream. I know there's https://gleam.run/

It's not possible, because functions, pattern matching, guards, typespecs and success typing are fundamentally incommensurable: each specifies and/or enforces a subset of the other, they are all useful in their own way, but not isomorphic.

Formal attempts have repeatedly failed, even when they exclude message passing, which is the most difficult (and most useful) aspect. If Wadler cannot do it, I'm sure I (or you) cannot.

A typesafe concurrent language is possible, but only a new language layer on top of E/E and the BEAM.

There is the set theoretic types work [1] lead by Jose and a couple of PhDs and also eqwalizer by WhatsApp [2]

[1] https://elixir-lang.org/blog/2022/10/05/my-future-with-elixi... [2] https://github.com/WhatsApp/eqwalizer