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

TL;DR

This paper introduces linking types, a novel approach that allows developers to annotate and reason about multi-language program components, ensuring safer interactions across different programming languages.

Contribution

It proposes linking types as a new method for reasoning about multi-language code interactions using annotations, enhancing safety and understanding.

Findings

Linking types enable reasoning about cross-language interactions.

Annotations help maintain behavioral guarantees across language boundaries.

The approach improves safety in multi-language software systems.

Abstract

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.