CS Colloquium
Date
Tuesday, January 27, 2026 10:00 - 12:00
Speaker
Ralf Jung (ETH Zurich)
Location
Raiffeisen Lecture Hall, Central Building
Series
Colloquium
Host
Michael Sammler
Contact
Rust is primarily known for its ownership-based type system that enables a low-level programming paradigm in a type-safe language. However, another key pillar of Rust is its treatment of unsafe code: while most languages tend to shun unsafe operations, often leaving them poorly specified, Rust gives unsafe operations a lot of attention, from a dedicated syntax to documentation and community norms. In this talk, I will explain this often-misunderstood aspect of Rust by talking about what unsafe Rust is, why it exists, how it is used, and how tooling and formal methods help mitigate the inherent risks of using unsafe operations.
Bio: Ralf Jung is an assistant professor at ETH Zrich, where he leads the Programming Language Foundations Lab within the Institute for Programming Languages and Systems in the Department of Computer Science. With a PhD from MPI-SWS and Saarland University under the supervision of Derek Dreyer, and postdoctoral experience in the PDOS group at MIT CSAIL, he has worked on the foundations of programming languages and applied verification to systems software. His primary research interests are Rust and Iris. His work has received numerous awards, such as a POPL Most Influential Paper Award and an Honorable Mention for the ACM Doctoral Dissertation Award. In collaboration with the Rust language team, his group is working to establish the formal foundations of Rust, particularly addressing the language's unsafe components. They are developing Miri, a tool for identifying Undefined Behavior bugs in unsafe Rust code, and working on MiniRust, a proposal for the precise specification of unsafe Rust. His long-term aim is to use formal verification to bring the full suite of Rust safety guarantees to unsafe Rust.