Safe Systems Programming in Rust: The Promise and the Challenge - Laboratoire Méthodes Formelles Accéder directement au contenu
Article Dans Une Revue Communications of the ACM Année : 2021

Safe Systems Programming in Rust: The Promise and the Challenge

Résumé

• Rust is the first industry-supported programming language to overcome the longstanding tradeoff between the safety guarantees of higher-level languages (like Java) and the control over resource management provided by lower-level "systems programming" languages (like C and C++). • It tackles this challenge using a strong type system based on the ideas of ownership and borrowing, which statically prohibits the mutation of shared state. This approach enables many common systems programming pitfalls to be detected at compile time. • There are a number of data types whose implementations fundamentally depend on shared mutable state and thus cannot be typechecked according to Rust’s strict ownership discipline. To support such data types, Rust embraces the judicious use of unsafe code encapsulated within safe APIs. • The proof technique of semantic type soundness, together with advances in separation logic and machine-checked proof, has enabled us to begin building rigorous formal foundations for Rust as part of the RustBelt project.
Fichier principal
Vignette du fichier
jung2020safe.pdf (616.91 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03021536 , version 1 (24-11-2020)

Identifiants

Citer

Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Derek Dreyer. Safe Systems Programming in Rust: The Promise and the Challenge. Communications of the ACM, 2021, 64 (4), pp.144-152. ⟨10.1145/3418295⟩. ⟨hal-03021536⟩
720 Consultations
622 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More