  Distributed programs are hard to get right because they are required to be
open, scalable, long-running, and tolerant to faults. In particular, the recent
approaches to distributed software based on (micro-)services where different
services are developed independently by disparate teams exacerbate the problem.
In fact, services are meant to be composed together and run in open context
where unpredictable behaviours can emerge. This makes it necessary to adopt
suitable strategies for monitoring the execution and incorporate recovery and
adaptation mechanisms so to make distributed programs more flexible and robust.
The typical approach that is currently adopted is to embed such mechanisms in
the program logic, which makes it hard to extract, compare and debug. We
propose an approach that employs formal abstractions for specifying failure
recovery and adaptation strategies. Although implementation agnostic, these
abstractions would be amenable to algorithmic synthesis of code, monitoring and
tests. We consider message-passing programs (a la Erlang, Go, or MPI) that are
gaining momentum both in academia and industry. Our research agenda consists of
(1) the definition of formal behavioural models encompassing failures, (2) the
specification of the relevant properties of adaptation and recovery strategy,
(3) the automatic generation of monitoring, recovery, and adaptation logic in
target languages of interest.
