Résumé
Toujours dans la problématique du passage à l’échelle des sémantiques mécanisées, le sixième séminaire a décrit des travaux récents sur la formalisation du langage Rust. Après avoir rappelé les concepts de base du système de types de Rust, notamment la possession et l’emprunt temporaire de structures de données mutables, l’orateur a décrit leur formalisation dans le système λ-rust. Les types y sont interprétés sémantiquement comme des formules de logique de séparation, ce qui permet de montrer la sûreté du typage même en présence de code « unsafe » non typable, pourvu que ce dernier soit vérifiable en logique de séparation. Ce travail débouche sur une suggestion d’amélioration de la sémantique de Rust : un modèle de partage de pointeurs appelé stacked borrows et qui permet de nouvelles optimisations lors de la compilation.
