RustWeek Interview: Andreea Costea, Rust as a Vehicle for Teaching and Formal Verfication

At RustWeek 2026, the Rust Project Content Team talks with Andreea Costea of TU Delft about formal verification, teaching Rust to students without a CS background, education in the age of LLMs, and analysis tools for detecting undefined behavior in unsafe Rust and FFI. Andreea shares how a fascination with abstraction led to a PhD in programming languages, five years of separation logic and verifying concurrent pointer-manipulating programs, and from there to Rust, which automatically addresses many of the problems formal verification struggled with. Topics include: - Why Rust's aliasing model is both what scares people and what draws them in, and how it builds pointer hygiene from the start - Teaching Rust as the introduction to programming in a ten-week software fundamentals course for embedded systems master's students with electrical engineering backgrounds: from hello world in week one to a Nintendo emulator in week ten - Adjusting explanations to each audience, and using visual tools to bridge the gap between what code does operationally and the invariants Rust enforces - Rethinking assessment in the age of LLMs: ungraded playground assignments, individual assignments with deliberately noisy specifications, and group projects where peers become the model - Detecting undefined behavior in unsafe Rust and FFI: a Rust front-end for Infer's incorrectness separation logic, dynamic analysis with Miri and MiriLLI, property-based testing to fuzz the "hot zone" just before calls into C, and hybrid static approaches - Letting the type system do the verification for programming in the large, and saving static analysis and formal verification for the small unsafe parts Andreea's RustWeek 2026 talk, "Lessons Learnt from using Rust as the Intro to Programming": https://www.youtube.com/watch?v=8iy37I0WE_s Links and resources: - Andreea's homepage: https://andrecostea.github.io/ - Programming Languages Group at TU Delft: https://pl.ewi.tudelft.nl/ - RustWeek 2026: https://2026.rustweek.org/ - Miri, a tool to detect undefined behavior in Rust: https://github.com/rust-lang/miri - MiriLLI, extending Miri across foreign function boundaries with an LLVM interpreter: https://github.com/icmccorm/mirilli - The MiriLLI paper, "A Study of Undefined Behavior Across Foreign Function Boundaries in Rust Libraries": https://arxiv.org/abs/2404.11671 - Infer, Meta's static analysis tool: https://fbinfer.com/ - Prusti, the ETH Zurich verifier built on the connection between Rust's type system and separation logic: https://github.com/viperproject/prusti-dev - Clippy: https://github.com/rust-lang/rust-clippy Interview conducted by Pete LeVasseur on behalf of the Rust Project Content Team. Find Pete at: - https://github.com/PLeVasseur/ - https://bsky.app/profile/petelevasseur.com