4 ms·

> Let us ask the question: Is there anything inherently unsafe about multiple (even mutable) references to an object? Yes. The ability to mutate an object nec

> Let us ask the question: Is there anything inherently unsafe about multiple (even mutable) references to an object? Yes. The ability to mutate an object necessarily implies the ability to mutate the state of an object to break guarantees. While there are definitely patterns where multiple mutable references to the same object can be safe, it is not inherently safe, and proving safety is far more challenging because you can't as easily rely on pre/postconditions for lemmas. The particular case that makes the utility of a one-mutable-xor-many-read-only model clear is something I trip over surprisingly frequently in C/C++: // Getting a value gets a pointer to somewhere in the hashtable... Value &V = hash_table[key]; // This may cause the hash table to grow, thereby invalidating said pointer... hash_table.insert(key2, value2); // ... and now I used it! V = meow; Sure, in a three-line function, it's kind of obvious (if you know to be aware of this possibility!), but in a function where the pointer and the use are separated by hundreds of lines of code, it's easy to miss that there is a requirement that the hash table not be resized between the two calls. With Rust, the fact that &mut for V means that I can't touch the hash table until I'm finished with V makes it a compiler error. Yeah, there are times when Rust's rule here pisses me off and feels too finicky, but it's also saved my butt several times. And quite frankly, a lot of the finicky can be worked around by building some solid container libraries to handle the cases where you can guarantee the safety with higher-level abstractions (say append-only data structures). More to the crux of the article however, I'm not generally impressed with automated theorem proving as a solution to safety. Already from the meat of the article, it seems that this solution is setting you up for using a complex language to specify the interface, which immediately begs the question of how you can be sure the interface is correctly specified.

akiarie 3y ago
> Already from the meat of the article, it seems that this solution is setting you up for using a complex language to specify the interface, which immediately begs the question of how you can be sure the interface is correctly specified. This is insightful. That is exactly what is happening, but our sense is that this language will be no more complicated than C itself, and will to a large extent parallel it. The question is really what is more effective, working under one set of constraints imposed universally (like the ownership semantics in Rust), or taking upon yourself the responsibility of defining such constraints within each program. In this way what we're doing is an application of the "trust the programmer" design philosophy; trust him, not only to know what he's doing, but to be able to express it (in the interface specification). > Sure, in a three-line function, it's kind of obvious (if you know to be aware of this possibility!), but in a function where the pointer and the use are separated by hundreds of lines of code, it's easy to miss that there is a requirement that the hash table not be resized between the two calls. With Rust, the fact that &mut for V means that I can't touch the hash table until I'm finished with V makes it a compiler error. It can seem as though the example we provide is contrived (because of course it is), but it is not mere contrivance. The point we stress the most is not that the bug is obvious if there are only three lines, but that the presence or absence of a bug is impossible to see even with a single function call whose interface is informal. So what is remarkable is not that we can write three lines of code that have or do not have an obvious error, but that by the mere fact of the interfaces being informal, a three-lined function can be impossible to analyse by itself. > The ability to mutate an object necessarily implies the ability to mutate the state of an object to break guarantees. While there are definitely patterns where multiple mutable references to the same object can be safe, it is not inherently safe, and proving safety is far more challenging because you can't as easily rely on pre/postconditions for lemmas. This doesn't answer the question. "it is not inherently safe" does not mean "it is inherently unsafe", it only means "it may be unsafe". So our point is that Rust precludes many kinds of programming that can be safe in relevant contexts, and this is what is so limiting.
- muldvarp 3y ago
  > That is exactly what is happening, but our sense is that this language will be no more complicated than C itself, and will to a large extent parallel it. The point of interfaces is usually to hide underlying complexity. What's the point of interfaces that are just as complicated as their implementation? > The question is really what is more effective, working under one set of constraints imposed universally (like the ownership semantics in Rust), or taking upon yourself the responsibility of defining such constraints within each program. One of the things I personally like about Rust is that its rules are very simple and still capture 95% of all situations I find myself in. Adding the complexity of having to write your own formal specifications for the remaining 5% doesn't seem like it's worth the effort. > So our point is that Rust precludes many kinds of programming that can be safe in relevant contexts, and this is what is so limiting. Xr0 will also either 1) reject programs that are safe or 2) accept programs that are unsafe. An (computable) algorithm that decides for every C program whether it is safe or not is mathematically impossible. Start implementing loops and you'll quickly see why the idea of provable correctness without any restrictions is doomed to fail. Not that similar projects don't exist: CBMC, Frama-C, ... How does Xr0 differ from those existing projects?
  - naasking 3y ago
    > The point of interfaces is usually to hide underlying complexity Specifications are typically less complex than implementations, so it won't be just as complex. One purpose of specifications is to encapsulate, but another purpose can be to specify a contract/protocol.
  - akiarie 3y ago
    > The point of interfaces is usually to hide underlying complexity. What's the point of interfaces that are just as complicated as their implementation? This is a pivotal question and our answer to it exposes one of our basic assumptions. Interfaces do hide underlying complexity, but that is not all that they do. They define our interaction with abstractions, which not only hide complexity, but reduce it by "abstracting". So what we find in practice is that the interfaces are not as complicated as the code, because all they define is what the higher levels of abstraction need to know to interact abstractly with the lower levels. > One of the things I personally like about Rust is that its rules are very simple and still capture 95% of all situations I find myself in. Adding the complexity of having to write your own formal specifications for the remaining 5% doesn't seem like it's worth the effort. Well this is great. If you like Rust, there's nothing wrong with that. But many C programmers don't feel this way. > Xr0 will also either 1) reject programs that are safe or 2) accept programs that are unsafe. An (computable) algorithm that decides for every C program whether it is safe or not is mathematically impossible. Start implementing loops and you'll quickly see why the idea of provable correctness without any restrictions is doomed to fail. Insightful again! This is all true. Note, however, that we aren't claiming not to impose restrictions. We're claiming that the restrictions should concentrate at a different place than where they concentrate in Rust. They should orbit around the interfaces. Xr0 is certainly imposing restrictions there. Moreover, we are in no way suggesting/claiming that we can deduce the safety of arbitrary C programs, which is the whole reason the annotations are required. We're claiming that we can help programmers who already understand why their code is safe express these reasons in relatively-simple annotations, and use these to verify their reasoning. Edit: typo.

akiarie 3y ago

> Already from the meat of the article, it seems that this solution is setting you up for using a complex language to specify the interface, which immediately begs the question of how you can be sure the interface is correctly specified. This is insightful. That is exactly what is happening, but our sense is that this language will be no more complicated than C itself, and will to a large extent parallel it. The question is really what is more effective, working under one set of constraints imposed universally (like the ownership semantics in Rust), or taking upon yourself the responsibility of defining such constraints within each program. In this way what we're doing is an application of the "trust the programmer" design philosophy; trust him, not only to know what he's doing, but to be able to express it (in the interface specification). > Sure, in a three-line function, it's kind of obvious (if you know to be aware of this possibility!), but in a function where the pointer and the use are separated by hundreds of lines of code, it's easy to miss that there is a requirement that the hash table not be resized between the two calls. With Rust, the fact that &mut for V means that I can't touch the hash table until I'm finished with V makes it a compiler error. It can seem as though the example we provide is contrived (because of course it is), but it is not mere contrivance. The point we stress the most is not that the bug is obvious if there are only three lines, but that the presence or absence of a bug is impossible to see even with a single function call whose interface is informal. So what is remarkable is not that we can write three lines of code that have or do not have an obvious error, but that by the mere fact of the interfaces being informal, a three-lined function can be impossible to analyse by itself. > The ability to mutate an object necessarily implies the ability to mutate the state of an object to break guarantees. While there are definitely patterns where multiple mutable references to the same object can be safe, it is not inherently safe, and proving safety is far more challenging because you can't as easily rely on pre/postconditions for lemmas. This doesn't answer the question. "it is not inherently safe" does not mean "it is inherently unsafe", it only means "it may be unsafe". So our point is that Rust precludes many kinds of programming that can be safe in relevant contexts, and this is what is so limiting.

muldvarp 3y ago
> That is exactly what is happening, but our sense is that this language will be no more complicated than C itself, and will to a large extent parallel it. The point of interfaces is usually to hide underlying complexity. What's the point of interfaces that are just as complicated as their implementation? > The question is really what is more effective, working under one set of constraints imposed universally (like the ownership semantics in Rust), or taking upon yourself the responsibility of defining such constraints within each program. One of the things I personally like about Rust is that its rules are very simple and still capture 95% of all situations I find myself in. Adding the complexity of having to write your own formal specifications for the remaining 5% doesn't seem like it's worth the effort. > So our point is that Rust precludes many kinds of programming that can be safe in relevant contexts, and this is what is so limiting. Xr0 will also either 1) reject programs that are safe or 2) accept programs that are unsafe. An (computable) algorithm that decides for every C program whether it is safe or not is mathematically impossible. Start implementing loops and you'll quickly see why the idea of provable correctness without any restrictions is doomed to fail. Not that similar projects don't exist: CBMC, Frama-C, ... How does Xr0 differ from those existing projects?
- naasking 3y ago
  > The point of interfaces is usually to hide underlying complexity Specifications are typically less complex than implementations, so it won't be just as complex. One purpose of specifications is to encapsulate, but another purpose can be to specify a contract/protocol.
- akiarie 3y ago
  > The point of interfaces is usually to hide underlying complexity. What's the point of interfaces that are just as complicated as their implementation? This is a pivotal question and our answer to it exposes one of our basic assumptions. Interfaces do hide underlying complexity, but that is not all that they do. They define our interaction with abstractions, which not only hide complexity, but reduce it by "abstracting". So what we find in practice is that the interfaces are not as complicated as the code, because all they define is what the higher levels of abstraction need to know to interact abstractly with the lower levels. > One of the things I personally like about Rust is that its rules are very simple and still capture 95% of all situations I find myself in. Adding the complexity of having to write your own formal specifications for the remaining 5% doesn't seem like it's worth the effort. Well this is great. If you like Rust, there's nothing wrong with that. But many C programmers don't feel this way. > Xr0 will also either 1) reject programs that are safe or 2) accept programs that are unsafe. An (computable) algorithm that decides for every C program whether it is safe or not is mathematically impossible. Start implementing loops and you'll quickly see why the idea of provable correctness without any restrictions is doomed to fail. Insightful again! This is all true. Note, however, that we aren't claiming not to impose restrictions. We're claiming that the restrictions should concentrate at a different place than where they concentrate in Rust. They should orbit around the interfaces. Xr0 is certainly imposing restrictions there. Moreover, we are in no way suggesting/claiming that we can deduce the safety of arbitrary C programs, which is the whole reason the annotations are required. We're claiming that we can help programmers who already understand why their code is safe express these reasons in relatively-simple annotations, and use these to verify their reasoning. Edit: typo.