With Xavier Denis!

Rust has shown how an advanced and strict type system can drastically reduce the complexity of systems programming: the borrow checker serves as both a programmer's worst foe and most loyal ally, preventing bugs along the way. But the type system of Rust only gets us so far—it does nothing to help us prove the functional correctness of our code. Xavier will show you how to change that by using Creusot, an experimental tool for contract-based verification of Rust code. We'll discuss a little of the theory and the practice behind Creusot, what it can do right now, and what its limitations are.

Xavier is a Ph.D. candidate at the Laboratoire des Methodes Formelles in Paris, where he studies the verification of Rust programs. He's interested in type theory, formal verification, and programming language design. In the long term, he'd like to work on making formal verification and theorem proving more approachable and tractable. In a past life, he was an SRE at Shopify, where he worked on core platform scalability. Offline, he likes to bake and will enjoy socializing in cafes when it's possible again.

This virtual talk was brought to you by the Berlin Functional Programming Group. Join us on Meetup: https://www.meetup.com/Berlin-Functio...​ Follow us on Twitter: https://twitter.com/BerlinFPGroup​ Buy a T-shirt: https://teespring.com/berlin-fp-group​ Support us on Patreon: https://www.patreon.com/bfpg​