You can mostly get the shapes of type-safety you'd typically expect to save you from yourself by being diligent about type specs and enabling:

  -Wunderspecs
  -Wunknown
  -Wunmatched_returns
  -Woverspecs
  -Wspecdiffs

And depending on a whole slew of things that may or may not make this useful, or more likely tractable for your codebase, you can enable this to track down some shapes of race conditions:

  -Wrace_conditions

The part where there's still a hole (now that most of the hole around Maps has been plugged) is in the message passing semantics. You can be conventional about how you write an API around the message passing to alleviate this, but there's still nothing stopping any random process from sending any shape of data to any other random process and thus essentially breaks Dialyzer's ability to enable static type checking through all paths. But as long as you have a catch-all matching clause implemented that dumps anything that doesn't explicitly match one of your types you're mostly fine.

> any chance Erlang-like supervision and actor model in general might make a comeback in Rust?

As a library, sure, but like green threads, actors aren't ideal for a systems language.

The guys at ETHZ thought otherwise with Active Oberon.

Interesting. Were actors available at the kernel level? If so, how?

Not actors. I should have been more explicit, as I was referring to green threads.

One could probably discover failures at compile-time with Erlang/Elixir as well, especially if one is diligent with typespecs and/or pattern matching / destructuring.

For example, if I have the following Elixir function definitions:

    def foo({:bar, bell}), do: IO.puts("got a barbell: #{bell}")
    def foo({:baz, bell}), do: IO.puts("got a bazbell: #{bell}")

Subsequently calling `foo({:bat, "some value for bell"})` should be detectable by the compiler and thus generate at least a warning. We can luckily catch it relatively easily and painlessly at runtime with Erlang's normal insistence on process supervision trees, but it's still a crash that could be easily avoided without having to jump into the realm of full-blown "defensive" programming.

Dyalizer solves your example already.

But finding race conditions is another problem entirely. Have a look at Concuerror and PropEr.