3 ms·

What the paper demonstrates is that if you have a correct borrow checker, and you have the ability to create types using `unsafe` which can extend the semantics

by lambda 9y ago

What the paper demonstrates is that if you have a correct borrow checker, and you have the ability to create types using `unsafe` which can extend the semantics of the language to cover things that the borrow checker cannot cover, you can write proofs that demonstrate that the language is still sound given the addition of those types. This helps demonstrate that one of the fundamental design goals of Rust, have a simple but limited system of borrowing built into the language, and allow more complex forms of managing reference types safely built on top of it as library features using `unsafe`, is a fundamentally sound design. In other words, you don't have to treat the language and all libraries using `unsafe` as one large system that you need to prove soundness of, but you can do modular proofs of the core language, and each library that adds a new type of memory and reference management, independently. Those bugs you reference are simply bugs in Rust's borrow checker. The language used for the RustBelt paper, LambdaRust, is a language that is much simpler than Rust itself, making the borrow checking much easier but the language not as convenient to use (it is not intended to be used at all, just to act as a model of Rust). The things you reference are simply bugs, but because of the fairly expressive syntax that Rust offers actually getting the borrow checker right can be be difficult in some cases. I don't think that there are any theoretical concerns about the ability to write a correct borrow checker, just practical issues with the current implementation not correctly handling certain cases.

bennofs 9y ago
> I don't think that there are any theoretical concerns about the ability to write a correct borrow checker, just practical issues with the current implementation not correctly handling certain cases. Is it really that trivial? When looking through https://github.com/rust-lang/rust/blob/master/src/librustc_borrowck/borrowck/README.md https://github.com/rust-lang/rust/blob/master/src/librustc_b..., it is not at all clear that these rules cover everything to me. There are some complex side conditions, isn't it easy to miss something there?
- kibwen 9y ago
  No-one is implying that writing a borrow checker is trivial. Proving it correct will take some work, though as your own link indicates the borrow checker was designed with formal reasoning in mind from the beginning.
- lambda 9y ago
  There is a large amount of room between "trivial" and "serious concerns that it will be impossible without fundamentally altering the language." All I was saying is that there aren't such serious concerns about the borrow checker; there are some known holes, but most people think it's just a matter of doing the work to fix those holes (which could be a lot of work, and involve significant refactoring), not that needs to be an entire change in the fundamental way the borrow checker works, or that borrow checking itself is theoretically unsound, or that some features of the language are fundamentally incompatible with sound borrow checking. The RustBelt work addressed one of the big open questions; is it possible to treat `unsafe` code in a modular fashion, or does all analysis of unsafe code have to consider all possible interactions with all other modules which use `unsafe` code as well? That was in many ways quite a big question about the design of Rust; can you prove or very each module which uses `unsafe` independently? The borrow checker, on the other hand, is an entirely local analysis. It can get quite complex, especially as you allow for more fine-grained borrow checking to make it convenient to use compound objects, and introduce non-lexical lifetimes which help reduce the number of restrictions on what you can do, but since it's entirely local, it's a much more tractable problem. I think that it would be good to eventually formalize the full Rust borrow checker, and of course it's always good to fix these soundness bugs, but there are some more important open questions right now like fully specifying Rust's memory model (https://github.com/nikomatsakis/rust-memory-model https://github.com/nikomatsakis/rust-memory-model) so it's possible to know what kinds of aliasing you can actually do in `unsafe` code, and which will be safe even under future versions of the compiler. The RustBelt work so far is just a nice foundation getting Rust to be more formally analyzed and specified. There's a lot of work left to be done.

by lambda 9y ago

bennofs 9y ago

> I don't think that there are any theoretical concerns about the ability to write a correct borrow checker, just practical issues with the current implementation not correctly handling certain cases. Is it really that trivial? When looking through https://github.com/rust-lang/rust/blob/master/src/librustc_borrowck/borrowck/README.md https://github.com/rust-lang/rust/blob/master/src/librustc_b..., it is not at all clear that these rules cover everything to me. There are some complex side conditions, isn't it easy to miss something there?

kibwen 9y ago
No-one is implying that writing a borrow checker is trivial. Proving it correct will take some work, though as your own link indicates the borrow checker was designed with formal reasoning in mind from the beginning.
lambda 9y ago
There is a large amount of room between "trivial" and "serious concerns that it will be impossible without fundamentally altering the language." All I was saying is that there aren't such serious concerns about the borrow checker; there are some known holes, but most people think it's just a matter of doing the work to fix those holes (which could be a lot of work, and involve significant refactoring), not that needs to be an entire change in the fundamental way the borrow checker works, or that borrow checking itself is theoretically unsound, or that some features of the language are fundamentally incompatible with sound borrow checking. The RustBelt work addressed one of the big open questions; is it possible to treat `unsafe` code in a modular fashion, or does all analysis of unsafe code have to consider all possible interactions with all other modules which use `unsafe` code as well? That was in many ways quite a big question about the design of Rust; can you prove or very each module which uses `unsafe` independently? The borrow checker, on the other hand, is an entirely local analysis. It can get quite complex, especially as you allow for more fine-grained borrow checking to make it convenient to use compound objects, and introduce non-lexical lifetimes which help reduce the number of restrictions on what you can do, but since it's entirely local, it's a much more tractable problem. I think that it would be good to eventually formalize the full Rust borrow checker, and of course it's always good to fix these soundness bugs, but there are some more important open questions right now like fully specifying Rust's memory model (https://github.com/nikomatsakis/rust-memory-model https://github.com/nikomatsakis/rust-memory-model) so it's possible to know what kinds of aliasing you can actually do in `unsafe` code, and which will be safe even under future versions of the compiler. The RustBelt work so far is just a nice foundation getting Rust to be more formally analyzed and specified. There's a lot of work left to be done.