Modal logic allows for reasoning about truth from multiple simultaneous perspectives. These perspectives, called “worlds,” are identified with the locations in the distributed program. This enables the programming language to be simultaneously aware of the various hosts involved in a program, their local resources, and their differing perspectives on each other’s code and data. This leads to a clean and general type structure for programs that respects locality while permitting high-level language features.
