"Formal semantics for multi-language programs" by Amal Ahmed

Multi-language programs are ubiquitous and language designers have long been designing programming languages to support interoperability. We've had platforms such as .NET, JVM, and COM that facilitate interoperability, and languages such as Scala, F#, SML.NET, and many more that treat it as a central design feature. In a 2007 paper, Matthews and Findler pointed out that most multi-language research was focused almost exclusively on how to implement interoperability efficiently and not on the quite subtle semantics of these features. They presented a multi-language semantics framework that gives language designers a methodology for taking two languages, adding interoperability boundaries between them, and giving an operational semantics to those boundaries. I'll describe the mechanics of multi-language semantics, how they support reasoning about the behavior of mixed-language programs, and discuss the impact that this tool has had in the last 15 years on research on compiler correctness, secure compilation, and the design and verification of safe FFIs.
Amal Ahmed
Professor, Northeastern University
Amal Ahmed is a Professor at the Khoury College of Computer Sciences at Northeastern University. Her interests include type systems and semantics, compiler verification, language interoperability, and secure compilation. Her earlier work showed how to scale the logical relations proof method to realistic languages, leading to wide use of the technique, including for soundness of advanced type systems such as Rust's, correctness of compiler transformations, and verification of fine-grained concurrent data structures. Her current work includes design and verification of safe FFIs and richer ABIs, and development of RichWasm, a richly typed WebAssembly that supports safe, shared-memory, inter-language linking. Over the last decade, she has been a frequent speaker and less-frequent organizer of the Oregon Programming Languages Summer School (OPLSS) and the Programming Languages Mentoring Workshop (PLMW), which seek to broaden participation in PL research.
----
Recorded on Sept 21, 2023 in the PWLConf track at Strange Loop 2023 in St. Louis, MO.
thestrangeloop.com
pwlconf

[@capability-snob]

If, like me, you need more of this, Amal Ahmed gave a brilliant class at OPLSS that is on youtube. It's sublimely interesting and presented with the same degree of enthusiasm and power on display here, and presents some truly intriguing design decisions that can be made at this boundary. I've been meaning to catch up with what her group are working on, so stoked to see she's at strange loop!

[@IDisposable]

Absolutely the best talk this year. I learned so much.

[@Etudio]

Excellent presentation! Thank you Amal! Miss you much. God bless RichWASM.

[@jimhrelb2135]

21:23 Jane Street just made this transition so so much better

[@valentinussofa4135]

Amazing👏She is a legend.

[@Tony-dp1rl]

16:28 I was a C programmer professionally for years in the 90's, and I remember Zero as success, not an error, in every system and code base I can recall. How odd that she said Zero is an error in C.

[@naturallyinterested7569]

With integer-valued functions that's true, you usually return negative values on error (e.g. most of linux kernel functions), but for pointers it's usually NULL, and I'm guessing from her pov that's the more likely case, as you usually pass your data across language boundaries by heap pointer (because stack and registers very bad for language interop).