Choreographies for Distributed Systems: Reasoning, Expressivity, and Development

Decades of research in computing led to high-level programming languages that can turn a programmer's ideas into executable software. For applications that run in isolation, we have a solid toolbox.

We can write code with abstract concepts like functions and objects, and then a compiler tool can automatically produce working implementations.

This significantly increases productivity, facilitates program analysis, and reduces the risk of bugs.Today, society increasingly relies on distributed systems for work, services, social participation, and so forth. Here the key high-level concept is that of communication: a message exchange between independent programs.

Yet it is nowhere to be found in the syntax of modern programming languages.

Instead, we manually write lower-level instructions for sending and receiving messages in separate programs, hoping that they match each other during execution and produce the wished communications.

This is infamously hard, leaving us with code that is difficult to write or trust.This situation is not due to lack of trying.

Choreographic programming is a recent attempt at a programming paradigm with high-level abstractions for communications and their composition in programs called choreographies. Unfortunately, compiling choreographies is technically challenging, which resulted in excessive simplification.

Current theories make unrealistic assumptions -- remaining confined to toy scenarios -- and reasoning methods for choreographies are underdeveloped.This project will break new ground by developing (a) new linguistic constructs for choreographies that can deal with realistic scenarios, (b) logics for verifying properties about choreographies and understanding what they mean for the compiled code, and (c) a toolchain for compiling, testing, and deploying software based on our choreographies.

These actions have the potential to significantly impact how we will model and program distributed applications in the future.