Patina : A Formalization of the Rust Programming Language
Patina : A Formalization of the Rust Programming Language
复制标题
DOI：
--
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Eric C. Reed
中科院分区：
文献类型：
--
作者：
Eric C. Reed
Rust是一种新的系统语言，它使用一些高级类型的系统功能，特别是仿射类型和区域，以确保记忆安全性并消除对垃圾收集器的需求。为了确保合并的系统，Rust还不知道它的区域（称为借用检查器），这是不正确的。由于Rust的目标是成为C/C ++的更安全的替代品，我们应该确保该安全方案实际上有效。安全，并描述了借用检查器的操作。此外，我们的模型提供了借用检查器的句法版本，这可能比Rust中的非句法版本更可理解。
Rust is a new systems language that uses some advanced type system features, specifically affine types and regions, to statically guarantee memory safety and eliminate the need for a garbage collector. While each individual addition to the type system is well understood in isolation and are known to be sound, the combined system is not known to be sound. Furthermore, Rust uses a novel checking scheme for its regions, known as the Borrow Checker, that is not known to be correct. Since Rust’s goal is to be a safer alternative to C/C++, we should ensure that this safety scheme actually works. We present a formal semantics that captures the key features relevant to memory safety, unique pointers and borrowed references, specifies how they guarantee memory safety, and describes the operation of the Borrow Checker. We use this model to prove the soudness of some core operations and justify the conjecture that the model, as a whole, is sound. Additionally, our model provides a syntactic version of the Borrow Checker, which may be more understandable than the non-syntactic version in Rust.