The Virtue of Busy Waiting

Hi all

Rafał will speak for us this month. Here are the details...

Abstract:

In 1977, Leslie Lamport proposed an approach to prove the correctness of multiprocess computer programs. Ten years later, Bowen Alpern and Fred Schneider came up with a formal representation of this approach,

that to this date seems to be _the_ way of teaching it on distributed and parallel programming courses.

The basis of this method is to distinguish between safety and liveness properties of the system we're building and then prove them empirically.

Safety properties tell us which states of the program are always forbidden. On the other hand, liveness properties describe the states that might be illegal at a particular moment in time, but as long as they will _eventually_ become valid later on, everything's fine with our system.

What does it have to do with programs we write in Elixir? Even if for most of the time we're not proving our programs formally, we're still doing our best to provide an "informal" proof. By writing tests we're trying to convince ourselves and other team members that our programs are good enough so that they provide expected value.

However, not many testing tools (not only those of Elixir) make a distinction between program properties, like those proposed by Lamport. Every time we write `assert` on some boolean condition, we're only doing as much as testing a _safety_ property.

In this presentation I would like to show you the value behind thinking about both kinds of properties when designing your system. After all, Lamport's motivation behind proving software correctness was high complexity of multi-process, asynchronous systems. These are canonical examples of programs that we all build using Elixir and Erlang programming languages.

Bio:

Rafal is a software engineer with 10 years of experience in Elixir, Erlang and C. He has worked on various distributed systems, ranging from tiny clusters on microcontrollers to some of the largest chat servers in the world. Having consulted on many real-world projects, he has come to believe that clean architecture, ruthless simplicity, and a principled stance towards testing for correctness are required for software to serve its business purpose successfully in the long run.