一句话：提出用可实现性模型形式化定义语言的 ABI，将高层抽象类型与底层代码相连，并首次形式化库演进。
ABI 规定了语言在其目标平台上的互操作规则（数据布局、调用约定等），编译器、库与外部函数接口都依赖它，但 ABI 通常以散文形式描述，其表达力与安全性长期停滞，远落后于源语言类型系统的演进。本文提出一种更丰富、更语义化的 ABI 愿景，并给出用可实现性模型（realizability model）形式化规约 ABI 的方法论，从而把高层抽象类型与笨重但行为良好的底层代码联系起来。作者以函数式源语言的 ABI 相对于类 C 目标语言中引用计数实现的规约为案例研究，其关键技术贡献是一个基于图的分离逻辑模型，借助受混合逻辑（hybrid logic）启发的模态刻画引用计数资源的所有权与可访问性。文中还展示不同设计决策如何被解释进语义 ABI，并首次形式化了 Swift ABI 的特色之一——库演进。
The Application Binary Interface (ABI) for a language defines the interoperability rules for its target platforms, including data layout and calling conventions, such that compliance with the rules ensures “safe” execution and perhaps certain resource usage guarantees. These rules are relied upon by compilers, libraries, and foreign- function interfaces. Unfortunately, ABIs are typically specified in prose, and while type systems for source languages have evolved, ABIs have comparatively stalled, lacking advancements in expressivity and safety. We propose a vision for richer, semantic ABIs to improve interoperability and library integration, supported by a methodology for formally specifying ABIs using realizability models. These semantic ABIs connect abstract, high-level types to unwieldy, but well-behaved, low-level code. We illustrate our approach with a case study formalizing the ABI of a functional source language in terms of a reference-counting implementation in a C-like target language. A key contribution supporting this case study is a graph-based model of separation logic that captures the ownership and accessibility of reference-counted resources using modalities inspired by hybrid logic. To highlight the flexibility of our methodology, we show how various design decisions can be interpreted into the semantic ABI. Finally, we provide the first formalization of library evolution, a distinguishing feature of Swift’s ABI.
@article{WagnerE024,
title = {Realistic Realizability: Specifying ABIs You Can Count On},
author = {Andrew Wagner and Zachary Eisbach and Amal Ahmed},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA2},
year = {2024},
doi = {10.1145/3689755}
}