One thing I'm not clear about: Is it currently allowed for unsafe code to violate the obligations that are checked by stacked borrows? In some points of the talk, you referred to this as a "new" proof obligation. But don't Rust developers already have this obligation when writing unsafe?
In principle, no. Most Rust compiler devs would say that you are relying on undefined or unspecified behaviour. (There's some subtlety here: there's the behaviour that LLVM considers undefined, A.K.A really really undefined behaviour that summons the nasal demons, and there's behaviour that it doesn't, but isn't "specified" by the Rust project, so it isn't guaranteed to continue working in the future.) However, this model isn't still officially adopted as THE aliasing model of the Rust language, it currently has a kind of "semi-official" status. There is separately a workgroup called unsafe guidelines workgroup, which is trying to formalize and document what is allowed and what is not for unsafe code. However, if I understand correctly, even it doesn't have the power to decide what is "officially" allowed and what is not, as it says on it's website (a Github README.md) that it's trying to come up guidelines that are to be considered as "recommendations". I'm sure that as these bits of work mature, there will eventually be a push to make official and set in stone what's allowed and what's not in unsafe code. This might be a separate effort from the current one's but the current ones are for sure going to "clear the way" there; we are gaining more and more experience of this stuff all the time.
As I understand, the compiler doesn't actually compile unsafe code differently. Like, if you wrap your entire program in unsafe { }, it doesn't change meaning. It's just that some constructs are not allowed in safe code.
It is certainly "allowed" in the sense that no one's stopping you. Just like you can have major C/C++ projects that do undefined behavior-important projects, like Chrome or the Linux kernel, which may do particular kinds of UB, whether on purpose for a good reason; or without knowing it's UB because not every C++ hacker wants to read a 300-page standard multiple times to know exactly what is UB; or due to bugs. It is further allowed in the sense that Stacked Borrows isn't even officially the rules of Rust. It's like this: right now, the meaning of unsafe pointer usage is "i dunno, whatever the compiler does -- which will be kind of like what a C compiler does" and even this makes Rust dramatically safer than C++. But we mostly agree there should be rules you can follow to ensure your unsafe code is *really* OK, and Stacked Borrows is the most credible, most worked-out vision of what those rules might be.
Very good talk! And I also want to take the opportunity to thank you for your excellent work on Rust.
Excellent talk. Exactly what I was looking for
One thing I'm not clear about:
Is it currently allowed for unsafe code to violate the obligations that are checked by stacked borrows?
In some points of the talk, you referred to this as a "new" proof obligation. But don't Rust developers already have this obligation when writing unsafe?
By the way, wonderfully done in 15 minutes!
In principle, no. Most Rust compiler devs would say that you are relying on undefined or unspecified behaviour. (There's some subtlety here: there's the behaviour that LLVM considers undefined, A.K.A really really undefined behaviour that summons the nasal demons, and there's behaviour that it doesn't, but isn't "specified" by the Rust project, so it isn't guaranteed to continue working in the future.) However, this model isn't still officially adopted as THE aliasing model of the Rust language, it currently has a kind of "semi-official" status.
There is separately a workgroup called unsafe guidelines workgroup, which is trying to formalize and document what is allowed and what is not for unsafe code. However, if I understand correctly, even it doesn't have the power to decide what is "officially" allowed and what is not, as it says on it's website (a Github README.md) that it's trying to come up guidelines that are to be considered as "recommendations".
I'm sure that as these bits of work mature, there will eventually be a push to make official and set in stone what's allowed and what's not in unsafe code. This might be a separate effort from the current one's but the current ones are for sure going to "clear the way" there; we are gaining more and more experience of this stuff all the time.
As I understand, the compiler doesn't actually compile unsafe code differently. Like, if you wrap your entire program in unsafe { }, it doesn't change meaning. It's just that some constructs are not allowed in safe code.
It is certainly "allowed" in the sense that no one's stopping you. Just like you can have major C/C++ projects that do undefined behavior-important projects, like Chrome or the Linux kernel, which may do particular kinds of UB, whether on purpose for a good reason; or without knowing it's UB because not every C++ hacker wants to read a 300-page standard multiple times to know exactly what is UB; or due to bugs.
It is further allowed in the sense that Stacked Borrows isn't even officially the rules of Rust. It's like this: right now, the meaning of unsafe pointer usage is "i dunno, whatever the compiler does -- which will be kind of like what a C compiler does" and even this makes Rust dramatically safer than C++. But we mostly agree there should be rules you can follow to ensure your unsafe code is *really* OK, and Stacked Borrows is the most credible, most worked-out vision of what those rules might be.