Content area
Distributed systems are a fundamental part of modern computing, but they are notoriously difficult to program. Developers must reason about a wide variety of non-deterministic behaviors, including message reordering, retries, and failures, all while also having to deal with the inherent concurrency across machines. Existing programming languages focus on local semantics, and provide little help reasoning about the global behavior of the distributed system.
In this dissertation, we present a new foundation for distributed programming that offers richer correctness guarantees and enables new opportunities for modularity. We develop a generalized notion of asynchronous streams that capture distributed semantics in types and restrict downstream behavior to guarantee determinism. Our model makes it possible to write an entire distributed protocol in a single function, encapsulating the network and concurrency. These building blocks can be composed to form complex distributed systems with strong correctness guarantees.
We reify this model in a Rust framework called Hydro. Hydro leverages staged programming to expose a high-level streaming interface while compiling down to bare-metal binaries with performance matching handwritten systems. We then explore optimization techniques for distributed systems enabled by our semantics, including program synthesis and term rewriting. Our work demonstrates that it is possible to build a practical programming model for distributed systems that is both correct and efficient, enabling developers to build more reliable and scalable software.