May 7-10, 2017 Asilomar, California
When implementing large software systems, programmers should be able to implement each part of the system using the programming language best suited to the task at hand. But current multi-language systems are difficult for programmers to reason about because components interact only after compilation to a lower-level target. The source-level contexts that programmers use to reason about their components no longer match the reality of the contexts that their components are running in. The additional contexts impact the notion of equivalence that justifies behavior-preserving modifications of code, whether programmer refactorings or compiler optimizations.
We advocate that language designers provide programmers with the means to reason about inputs from “other” languages, but in a way that remains close to the semantics of their language. Linking types are a well-specified minimal extension of the source language that allow programmers to optionally annotate where in their programs they can link with components that would not be expressible in their unadulterated source language, giving them fine-grained control over the contexts that they must reason about and the equivalences that arise.