4 ms·

I work on proving things about unsafe Rust for my day job, and you really don't know what you're talking about if you think what you're proposing would be remot

I work on proving things about unsafe Rust for my day job, and you really don't know what you're talking about if you think what you're proposing would be remotely sufficient to guarantee safety in a modern systems language. I'm not saying a way to deal with uninitialized data would not help, but that is not the primary source of potential unsafety in Rust, and it's completely infeasible for the language to include all the features that would be required to prove all unsafe Rust code safe (at least, given what we know now--if you have ideas about weak memory that I'm not aware of, feel free to ping me!). However, it is possible to do machine-checked proofs about unsafe Rust, and once those proofs are done, they remain valid forever, so I'd prefer the current approach (which is to verify the standard library and some major third party ones, and make the tooling for proving correctness of other Rust libraries as easy as possible).

Animats 9y ago
Of course it's not sufficient. It does make possible to talk about partially initialized arrays, which is a necessary step to checking their access, either at run time or by formal methods. The "Weak" problem is mostly a back-pointer problem. If you had some way to talk about a back pointer locked in an invariant relationship with a forward pointer, that would deal with back pointers for trees and such. I sketched out a solution for this on YC earlier this year.[1] This doesn't deal with true circular lists, but those are relatively rare; people tend to use arrays for that today. It's good to hear this criticized from someone who does program proving. I used to do that, a long time ago. What I usually get from the Rust crowd is macho assertion that they don't need checking of their unsafe code. History and the CERT archives indicate they do. [1] https://news.ycombinator.com/item?id=14302823 https://news.ycombinator.com/item?id=14302823
- Jweb_Guru 9y ago
  Weak memory isn't related to weak pointers. What you're referring to is actually pretty easy to deal with (well, not easy, it's pretty tedious to prove in most of the individual cases, but it's not conceptually difficult). Weak memory refers to atomic operations with weak consistency (like relaxed, release-acquire, and perhaps most confoundingly consume). Modeling them along with lifetimes and ownership tracking requires a fairly sophisticated language model with lots of intermediate tokens and ghost state, which would be a tremendous burden to include in a programming language. Fortunately, it looks like most features of safe Rust extend straightforwardly to weak memory models, but that isn't always the case for unsafe Rust.

Animats 9y ago

Of course it's not sufficient. It does make possible to talk about partially initialized arrays, which is a necessary step to checking their access, either at run time or by formal methods. The "Weak" problem is mostly a back-pointer problem. If you had some way to talk about a back pointer locked in an invariant relationship with a forward pointer, that would deal with back pointers for trees and such. I sketched out a solution for this on YC earlier this year.[1] This doesn't deal with true circular lists, but those are relatively rare; people tend to use arrays for that today. It's good to hear this criticized from someone who does program proving. I used to do that, a long time ago. What I usually get from the Rust crowd is macho assertion that they don't need checking of their unsafe code. History and the CERT archives indicate they do. [1] https://news.ycombinator.com/item?id=14302823 https://news.ycombinator.com/item?id=14302823

Jweb_Guru 9y ago
Weak memory isn't related to weak pointers. What you're referring to is actually pretty easy to deal with (well, not easy, it's pretty tedious to prove in most of the individual cases, but it's not conceptually difficult). Weak memory refers to atomic operations with weak consistency (like relaxed, release-acquire, and perhaps most confoundingly consume). Modeling them along with lifetimes and ownership tracking requires a fairly sophisticated language model with lots of intermediate tokens and ghost state, which would be a tremendous burden to include in a programming language. Fortunately, it looks like most features of safe Rust extend straightforwardly to weak memory models, but that isn't always the case for unsafe Rust.