May 7-10, 2017 Asilomar, California
Software developers compose systems from components written in many
different languages. A business-logic component may be written in Java
or OCaml, a resource-intensive component in C or Rust, and a
high-assurance component in Coq. In this multi-language world, program
execution sends values from one linguistic context to another. This
boundary-crossing exposes values to contexts with unforeseen
behavior—that is, behavior that could not arise in the source language
of the value. For example, a Rust function may end up being applied in
an ML context that violates the memory usage policy enforced by Rust’s
type system. This leads to the question of how developers ought to
reason about code in such a multi-language world where behavior
inexpressible in one language is easily realized in another.
This paper proposes the novel idea of linking types to address the
problem of reasoning about single-language components in a multi-lingual
setting. Specifically, linking types allow programmers to annotate where
in a program they can link with components inexpressible in their
unadulterated language. This enables developers to reason about
(behavioral) equality using only their own language and the annotations,
even though their code may be linked with code written in a language
with more expressive power.