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.

Are you saying Gleam has failed?

Are you aware of any of the recent advances?

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

In addition to gleam, there's also ongoing attempts to add static typing to Elixir.

There are plans to introduce type system into Elixir:

https://elixir-lang.org/blog/2023/06/22/type-system-updates-...