What:
Modern software systems are highly distributed and rely on global infrastructure vulnerable to grid failures, natural disasters, and malicious actors.
Resilient systems must be aware of where they are deployed and be equipped with mechanisms to shift workloads away from degraded regions.
We aim to build programming languages with strong safety guarantees for building these systems reliably.

How:
Programming such systems is difficult and error-prone. We propose extending programming languages with novel type and effect systems that model the physical location of data as part of the effect language, enabling developers to reason about effects on that data in a distributed setting. In particular, we aim to rule out a class of bugs we call "the right effect, but the wrong location."

Why:
These bugs are especially insidious, as they execute correctly but violate the implicit data model of the entire system. A misplaced effect can corrupt customer data, which is particularly dangerous for critical applications in healthcare or finance. It can also prevent the proper removal of data, resulting in regulatory non-compliance and violations of user privacy rights.

‍