3 ms·

> 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 implementati

> 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.

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.