Linking Types for Multi-Language Software: Have Your Cake and Eat It Too

Large software systems are and should be implemented with many different languages, each suited to the domain of the task at hand. High-level business logic may be written in Java or OCaml, resource-intensive components may be written in C or Rust, and high-assurance components may be written in Coq. In some development shops, domain-specific languages are used in various parts of systems to better separate the logic of particular problems from the plumbing of general-purpose programming. But how are programmers to reason about such multi-language systems? Currently, for a programmer to reason about a single source component within this multi-language system, it is not sufficient for her to consider how her component behaves in source-level contexts. Instead, she is required to understand the target contexts that her component will be run in after compilation - which requires not only understanding aspects of the compiler, but also how target components are linked together. These target contexts may have behavior inexpressible in the source, which can impact the notion of equivalence that justifies behavior-preserving modifications of code, whether programmer refactorings or compiler optimizations. But while programmers should not have to reason about arbitrary target contexts, sometimes multi-language linking is done exactly to gain access to features unavailable in the source. To enable programmers to reason about components that link with behavior inexpressible in their language, we advocate that language designers incorporate specifications for linking into the source language. Such specifications should allow a programmer to reason about inputs from other languages in a way that remains close to the semantics of her language. Linking types are a well-specified minimal extension of a source language that allow programmers to annotate where in their programs they can link with components that are not expressible in their unadulterated source language. This gives them fine-grained control over the contexts that they must reason about and the equivalences that arise.