دورية أكاديمية
Safe Systems Programming in Rust: The Promise and the Challenge
| العنوان: | Safe Systems Programming in Rust: The Promise and the Challenge |
|---|---|
| المؤلفون: | Jung, Ralf, Jourdan, Jacques-Henri, Krebbers, Robbert, Dreyer, Derek |
| المساهمون: | Max Planck Institute for Software Systems (MPI-SWS), Centre National de la Recherche Scientifique (CNRS), Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Université Paris-Saclay, Delft University of Technology (TU Delft) |
| المصدر: | ISSN: 0001-0782. |
| بيانات النشر: | HAL CCSD Association for Computing Machinery |
| سنة النشر: | 2021 |
| مصطلحات موضوعية: | Rust, safety, control, programming language, type systems, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], [INFO.INFO-PF]Computer Science [cs]/Performance [cs.PF], [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL] |
| الوصف: | International audience ; • 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. |
| نوع الوثيقة: | article in journal/newspaper |
| اللغة: | English |
| العلاقة: | hal-03021536; https://hal.science/hal-03021536Test; https://hal.science/hal-03021536/documentTest; https://hal.science/hal-03021536/file/jung2020safe.pdfTest |
| DOI: | 10.1145/3418295 |
| الإتاحة: | https://doi.org/10.1145/3418295Test https://hal.science/hal-03021536Test https://hal.science/hal-03021536/documentTest https://hal.science/hal-03021536/file/jung2020safe.pdfTest |
| حقوق: | info:eu-repo/semantics/OpenAccess |
| رقم الانضمام: | edsbas.3E63B82A |
| قاعدة البيانات: | BASE |
| DOI: | 10.1145/3418295 |
|---|