Rust & Prusti: From a Safety-Focused Design To Formal Verification
Event start time 19.11.2020 16:15
Event end time 19.11.2020 18:15
Did you hear that Rust looks very promising but wonder whether it's just hype? Are you interested in understanding why Rust is frequently mentioned as one of the most beloved programming languages? Do you want to know which features are truly unique to Rust?
In this talk, we discuss what makes Rust a modern systems programming language. Apart from its key features and guarantees, we consider frequently misunderstood concepts, such as unsafe code, and how they are supposed to be applied. Moreover, we demonstrate that the Rust compiler's powerful type system and safety guarantees can be further exploited to enable lightweight formal verification of functional correctness properties.
Agenda
- Introduction: What Rust can(not) do for you
- Rust in a Nutshell
- A dive into Rust's distinguishing features: ownership, borrowing, lifetimes, and traits
- How (should) programmers use Unsafe Rust?
- Prusti: Leveraging the Rust compiler for formal verification
Administrative Details
The talk will be held over Zoom and the link will be sent shortly before the talk.
Event organisers
Main event organiser Simon Meinhard