The Application Binary Interface (ABI) for a language specifies the interoperability rules for each of its target platforms, including properties such as data layout and calling conventions, such that compliance with the rules will ensure “safe” execution and perhaps provide certain guarantees about resource usage. These rules are relied upon by compilers for that language and others, libraries, and foreign-function interfaces. Unfortunately, ABIs are typically specified in prose and, while type systems for source languages have grown richer over time, ABIs have largely remained the same, lacking analogous advances in expressivity and safety guarantees.

We outline a vision for richer, semantic ABIs that would facilitate safer interoperability and library integrations, supported by a methodology for formally specifying ABIs using realizability models. These semantic ABIs relate abstract, high-level types to unwieldy, but well-behaved, low-level code. We demonstrate the approach with a case study that formalizes the ABI of a functional source language in terms of a reference-counting implementation in a C-like target language. A significant contribution is our reference-counting realizability model which uses a novel extension to separation logic that captures how each reference owns a share to the reference-counted resource. To demonstrate the value of a semantic ABI as an analytical tool, we show how several different practically-motivated design decisions can be interpreted in the semantic ABI. Finally, we give the first formalization of a Swift-style ABI with library evolution.