Framework enables reasoning across programs in multiple languages
Multi-language Program Logics
Programming Languages
Summary
Programs often combine code written in different programming languages, like C and assembly, but verifying such mixed-language programs has been difficult. The authors created Hotpot, a framework that lets developers reason about programs that use multiple languages together in a unified way. Hotpot includes methods to handle calls between languages, track shared memory, and reuse specifications across languages. This helps ensure that programs working across language boundaries behave correctly.
What this means in practice
- •For systems software developers: Verify correctness of programs combining high-level languages with low-level libraries using a uniform logic framework.
- •For compiler engineers: Integrate Hotpot to support formal verification of compiler output spanning multiple source and target languages.
Authors
Alexander Loitzl, Niklas Mück, Michael Sammler
Abstract
Real-world programs are rarely written in a single language: For example, C programs call assembly routines, and high-level languages like OCaml link with low-level C libraries. Yet program logics---one of the most successful techniques for modular program verification---almost exclusively target single-language programs. We present Hotpot, the first framework for building multi-language program logics. Hotpot enables compilation-independent, cross-language reasoning about languages with heterogeneous views of shared state. Hotpot rests on four key ideas: abstract calls to specify calls to unknown functions, lanes and the switching modality to move between languages inside the program logic, uniform integration of refinement reasoning via lanes, and exchanges to translate between separation logic assertions of different languages. We demonstrate that Hotpot allows reusing specifications across implementations in different languages, supports reasoning about higher-order cross-language function calls, and integrates with verified compilation. Hotpot is built on top of Iris and DimSum and mechanized in the Rocq Prover.