Write a Blog >>

Software today is overwhelmingly constructed in multiple languages. A major benefit of high-level languages is the increased reasoning power provided by their restrictions on program behavior. These increased reasoning principles could span from simple safety properties, such as memory-safety in Java, to complex correctness properties in dependently-typed languages. Unfortunately, when composing high-level languages with code written in other languages, these guarantees are not necessarily preserved. For example, if composing code written in Rust and Haskell, Haskell may duplicate a reference that Rust expects to be owned linearly, breaking Rust’s memory-safety guarantees. We argue for a unified approach to designing FFIs based on translations between types in the source languages that preserve different properties. We also describe a spectrum of safety properties for FFIs, and show examples of this approach producing various points on the spectrum for FFIs between a language with affine references and one with only unrestricted references.