effpi

Here’s a cool new project: effpi is being added to the Dotty community build.

I recommend just taking a read through the effpi page (which is quite short) for an overview. Basically, it appears to be an even-more-strongly-typed version of a message passing architecture — sort of like Akka Typed, but with a compiler plugin to prove some aspects of program correctness. More details can be found in this PDF.

As a longtime Akka geek, I think this is pretty exciting stuff: folks have been working on trying to put Actor architectures on a firmer theoretical footing for some time — the “pi calculus” is an important part of this, hence the name of effpi. Akka Typed has done a lot to make Akka less ad-hoc than classic Akka, but being able to reason better about your code’s message-passing logic and have confidence that you are avoiding deadlocks — that would be a big deal if it can be moved into day-to-day coding.

Mind, this isn’t a production system or anything like that: it’s pretty clearly a research project. But it’s an immensely practical research project, and I hope it proves successful. It addresses some of the standard complaints about Akka, and if these ideas get picked up and evolved, it might move the needle towards being able to use that in a really principled way.