Vous pouvez vous abonner à nos annonces de séminaires http://gallium.inria.fr/seminaires/ S E M I N A I R E __ / _` _ / / o / ) __) / / / / / /\/| (___/ (_/ (_ (_ / (__/ / | I N R I A - Paris 2 rue Simone Iff (ou: 41 rue du Charolais) Salle Lions 1, bâtiment C Lundi 9 janvier, 10h30 --------------------- Jacques-Henri Jourdan --------------------- MPI-SWS ============================================= Formalizing the essence of Rust's type system with the Iris separation logic ============================================= The 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.