Séminaire des équipes de recherche
Formalizing the essence of Rust's type system with the Iris separation logic
- Date : 9/01/2017
- Lieu : Inria de Paris, 2 rue Simone Iff, 75012 Paris - Salle Jacques-Louis Lions 1, bâtiment C - 10h30
- Intervenant(s) : Jacques-Henri Jourdan- MPI-SWS
He Rust programming language, whose first version has been recently released by Mozilla, gives high performance and low-level control over the machine's resources. However, contrary to other systems programming languages such as C or C++, its type system provides
strong safety guarantees. They include memory safety, but also no undesired aliasing and absence of data races. In order to fulfill these two apparently opposed objectives, Rust follows an ownership discipline based on a so-called "borrowing" mechanism.
In this talk, I will give a brief overview of the main features of Rust. I will explain why giving a formal proof of soundness of this type system is an interesting challenge. I will present our ongoing project of formalizing a core fragment using the recently developed Iris concurrent separation logic, of which I will give a brief overview.
Even more challenging, the standard library of Rust contains data structures providing "interior mutability". These data structures allow to mutate aliased pointers while keeping the strong guarantees by following carefully designed rules enforced statically or dynamically.