Open Collections

Formalizing Rust traits

University of British Columbia

Rust is a new systems programming language designed with a focus on bare metal performance, safe concurrency and memory safety. It features a robust abstraction mechanism in the form of traits, which provide static overloading and dynamic dispatch. In this thesis, we present MiniRust—a formal model of a subset of Rust. The model focuses on the trait system and includes some advanced features of traits such as associated types and trait objects. In particular, we discuss the notion of object safety—the suitability of a particular trait for creating trait objects—and we formally determine very general conditions under which it can be guaranteed. To represent the runtime semantics of MiniRust programs, we develop an explicitly-typed internal language RustIn, for which we prove type safety, and we show that well-typed MiniRust programs can be translated to well-typed RustIn programs. Finally, we adapt the informally-described Rust trait coherence rules to our model and we show that they are sufficient to ensure that overloads are always well-determined, even in the presence of library extensions.

Text

2015-12-01

Attribution-NonCommercial-NoDerivs 2.5 Canada

http://hdl.handle.net/2429/55609

Computer Science

University of British Columbia

UBCV

http://creativecommons.org/licenses/by-nc-nd/2.5/ca/