2019年03月06日に初出の投稿

Last modified: 2019-03-06

Rust is a major advancement in industrial programming languages due in large part to its success in bridging the gap between low-level systems programming and high-level application programming. This success has ultimately empowered programmers to more easily build reliable and efficient software, and at its heart lies a novel approach to ownership that balances type system expressivity with usability.

In this work, we set out to capture the essence of this model of ownership by developing a type systems account of Rust's borrow checker. To that end, we present Oxide, a formalized programming language close to source-level Rust (but with fully-annotated types). This presentation takes a new view of lifetimes as approximate provenances of references, and our type system is able to automatically compute this information through a flow-sensitive substructural typing judgment for which we prove syntactic type safety using progress and preservation. The result is a simpler formulation of borrow checking - including recent features such as non-lexical lifetimes - that we hope researchers will be able to use as the basis for work on Rust.

Oxide: The Essence of Rust

危険なコード(脆弱性やバグ)を作り込みにくいという触れ込みのある Rust だが、それを Oxide という形式的なモデルを作って論証してしまおうというアプローチの成果だ。たまに、或るプログラミング言語がチューリング完全かどうかという論証をやってる事例があるけれど、同じようにこういう形式的なアプローチで成果を持ち寄るのは非常に良いことだ。正直、ソーシャル・ブックマークのサイトなどでインフルエンザの流行みたいに何度も出てくる、「PHPの何がクソか」とか「emacs vs. IDE」みたいな宗教戦争など、どれほどロートルどもが膨大な昔話を穿り返したりハックを披歴しようと、はっきり言って「文明」というスケールでは些末な雑談でしかない。

  1. もっと新しいノート <<
  2. >> もっと古いノート

冒頭に戻る


※ 以下の SNS 共有ボタンは JavaScript を使っておらず、ボタンを押すまでは SNS サイトと全く通信しません。

Twitter Facebook