Nearly all modern systems critically depend on interoperability between languages and libraries, but reasoning formally about this interaction has proven to be a serious challenge, as different components maintain drastically different invariants. Recent efforts to tackle the interoperability problem make use of advanced type systems that relate types or behaviors in one language to those in another.

But as we descend down toward the binary layer, the sophisticated type machinery slowly disappears, and all that remains is an unspoken promise between components. This promise is the application binary interface (ABI), which specifies data layouts, calling conventions, and other low-level details required for interaction. But while type systems have grown richer, 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. Building on recent work, we suggest a way forward using realizability models, which formally relate abstract, high-level types to unwieldy, but well-behaved, low-level code. We motivate the approach with a case study that formalizes the ABI of a simple functional source language in terms of a reference counting target implementation.