A Concurrency System for Idris and Erlang

Quite interesting. It's an Idris interface that wraps around the Erlang primitives and OTP behaviors so as to generate Erlang code from a verified Idris implementation.

It's an interesting way to get around the dynamically typed nature of Erlang, as some of its properties have meant that despite several attempts, no one has managed to retrofit a complete type system yet, though Dialyzer provides approximate inference, in a similar manner to what I believe is a SAT solver.

Nonetheless, it's worth noting that Erlang's dynamically typed nature is nowhere near as much of an impediment as in other languages precisely due to fault tolerance guarantees from preemptively scheduled isolated actors and standard OTP behaviors providing supervision links, plus the fact that you pattern match on literal values. This and the encapsulation provided by modules leads to a remarkable system resilience even without much of a typing discipline, which shows that robust systems should have many other properties besides the type system.

Even still, anything to formally verify Erlang behaviors is a welcome advance. A rigorous approach is likely to uncover plenty of bugs and strengthen BEAM, which in turn will improve Elixir and others as well.

I like his Simpsons reference at the end there.