© 2019 Strange Loop
As software becomes increasingly complex, we need toolchains that simplify building systems using a mix of languages so we can use the best language for each part of a system. That "best" language might be Rust for a high-performance component, a terminating domain-specific language for a protocol parser, or a general-purpose scripting language for UI code.
Ideally, we should be able to reason only in our chosen language when working on that component. Unfortunately, most current languages and toolchains were designed with language interoperability as an afterthought, so they lack the means to support single-language reasoning when building multi-language software. For instance, we can reason about safe memory usage in Rust, but if our Rust component shares references with a Java method, we must reason about the possibility that Java might violate Rust's borrowing discipline leading to unsafe memory use.
This talk is about how to change the status quo to make it easier to build multi-language software. I'll argue that language designers should equip their "core" language with extensions, dubbed linking types, that allow programmers to annotate how their components should interact with features missing from their core language. Moreover, toolchain developers should devise compilers and linkers that prevent linking with external code that violates safety or security properties provided by the core language, unless the programmer uses linking-type annotations to request such linking.
Amal Ahmed is an Associate Professor of Computer Science at Northeastern University. She was previously an Assistant Professor at Indiana University and a Research Assistant Professor at the Toyota Technological Institute at Chicago. Her research interests lie in programming languages and compiler verification, with a focus on type systems, semantics, secure compilation, safe language interoperability, and gradual typing. She is known for her work on scaling the logical relations proof method to realistic languages---with features like memory allocation and mutation, objects, and concurrency---leading to wide use of the technique, e.g., for correctness of compiler transformations, soundness of advanced type systems, and verification of fine-grained concurrent data structures. Her primary focus for the last few years has been on developing an architecture for building correct and secure compilers that support safe inter-language linking of compiled code. Her awards include an NSF Career Award, a Google Faculty Research Award, and a George Van Ness Lothrop Fellowship. She has served as program chair for ESOP and on the steering committees of ETAPS, ESOP, PLMW, and ICFP. She is also a frequent lecturer at the annual Oregon Programming Languages Summer School (OPLSS).