Full abstraction can be used to specify that a compilation process preserves equational reasoning on the source language – in other words, the semantics of the low-level target language does not leak into source programs.

Abstraction leaks are not only compiler and system security issues, but also usability issues. Multi-language programming systems are widely used, but often exhibit unfortunate, unplanned interactions. We use full abstraction for language design, to specify that the languages of a multi-language system interact gracefully – in a way that is also, in particular, amenable to secure compilation.

We demonstrate our approach by the case-study of a proposed multi-language design that combines a simple ML language with a linear language with linear mutable state. We prove that programmers knowing only the ML side of the story will not have bad surprises when interacting with other code that may, internally, use the linear language.