A transformation between languages is fully abstract if it preserves observational equivalence. Full abstraction has been proposed as a desirable formal property of compilers: a fully-abstract compiler guarantees that the semantics of the low-level target language does not leak into source programs.

Abstraction leaks are also usability issues. Multi-language programming systems are widely used, but often exhibit unfortunate, unplanned interactions. We propose to use full abstraction for language design: if the embedding of a single language into the multi-language system is fully abstract, we know that it interacts gracefully with the other languages of the system.

We demonstrate our approach by a 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 code that may, internally, use the linear language.