4 ms·

The scope of unsafe ends at the next abstraction boundary. This means that everything outside of the std::vec module does not have to worry about Vec.

The scope of unsafe ends at the next abstraction boundary. This means that everything outside of the std::vec module does not have to worry about Vec. ... Of course, this also means that everything inside std::vec is potentially dangerous and needs to be proven to respect the semantics of Vec. So wait, in a nutshell, a module is 'safe' if and only if you formally prove that every public interface into the module and every way that public interface can be invoked... is error free. How is that any improvement on any other language? If the burden of 'safety' is formal proof of the entire module, then you're (surely) no better off than using C++ and doing exactly the same thing. I mean, obviously the borrow checker can help to some extent, but what you're basically saying is that it's not enough; you can't trust the borrow checker for safety; you must formally verify a module in order to know it's safe, if it contains any unsafe code. In other words, if your rust program has any module in any dependency that has unsafe code (ie. every rust program), it is potentially unsafe, regardless of the borrow checker (because some code path may invoke a 'safe' function that has not be formally verified to be safe, and results in undefined behaviour despite being safe). That's quite a troubling conclusion.

Jweb_Guru 11y ago
> How is that any improvement on any other language? Rust provides more facilities for exposing efficient, safe interfaces to unsafe code than do many other languages. The existence of safe and unsafe are not particularly interesting by themselves.
- shadowmint 11y ago
  Perhaps... but if you have to formally verify the entire module, those facilities aren't doing much good are they?
  - Jweb_Guru 11y ago
    You don't have to formally verify the entire module. The module "just" has to be correct :P. Additionally, very often, unsafe code is used in ways that cannot contaminate the entire module (that's the ideal, in fact), and the module that the unsafe code is used in is made deliberately small.
dbaupp 11y ago
I'm not really sure what the problem is here: having to formally verify a module doesn't seem fundamentally different to formally verify a single function. I mean, sure, it's some more code, but there's still well-defined containment. And, being "allowed" to reason about a whole module (well, usually one just cares about a whole type, but these often match, especially for unsafe code) seems far more useful: one can build far more interesting abstractions. If one was forced to reason about a single function at a time, Vec couldn't exist in a useful way, as every function would have to assume the incoming Vec value could be arbitrarily invalid. In any case, there are many many modules with no `unsafe` code, e.g. std::option has none [1], iron::response has none [2], image::jpeg has none [3] (just some random examples). These are automatically safe, if you assume that that the code they call is safe, which seems to me like the only assumption that can make sense: if the safe modules call unsafe ones that aren't safe... well, the problem is in the unsafe ones, not the safe ones. What I'm trying to say is this paragraph doesn't seem to change anything fundamental about the objections to safe vs. unsafe you sometimes write about; it is not introducing anything new, and so the refutations you often receive still apply. [1]: https://github.com/rust-lang/rust/blob/dfaddb732ced1da9d310990df095ca36f43fbc3d/src/libcore/option.rs https://github.com/rust-lang/rust/blob/dfaddb732ced1da9d3109... [2]: https://github.com/iron/iron/blob/d3942d72e3178e7b34ebf1ea0e07b2dc3f9749ee/src/response.rs https://github.com/iron/iron/blob/d3942d72e3178e7b34ebf1ea0e... [3]: https://github.com/PistonDevelopers/image/tree/f2b86c1ec6d3c02b827190671ea9302716e86028/src/jpeg https://github.com/PistonDevelopers/image/tree/f2b86c1ec6d3c...
- shadowmint 11y ago
  Well, given the most common refute of my concerns is 'you just have to make sure your unsafe blocks are verified to be correct', and the point of this article, is explicitly that this isnt the case... Now its that you have to just make sure all your code is correct, not just the unsafe blocks. /me shrugs I think thats lame, and breaks the promises rust is trying to make about writing safe secure software. If safe code may not be safe, whats the point of it at all. You, are of course welcome to your own oppinion.
  - kibwen 11y ago
Manishearth 11y ago
It seems like you're assuming the post is saying that you need formal verification to write safe Rust? I don't think that's the case. Note that the blog post is explicitly in the context of formally verifying Rust and its stdlib. This is not something that's necessary for a "good enough" guarantee that stuff works and is safe. The conclusion you can make is that formally verifying Rust is just as hard as C++ (I'm not sure I agree with this either, but it's really irrelevant), but this doesn't make Rust a worthless language since formal verification is not what you care about for everyday safety guarantees. > If the burden of 'safety' is formal proof of the entire module, then you're (surely) no better off than using C++ and doing exactly the same thing. Well, formal verification is nice, but it's not necessary. Take the Vec<T> interface for example. There are a couple of unsafe methods in it, and the invariant "len is always a valid length". It's easy to check if len is being modified elsewhere. It's easy to reason about these invariants. And it's easy to reason that it upholds the invariants that Rust expects for safe functions. Formal verification is harder, but practical verification is easier since it's contained in a small surface area. On the other hand, there's no "containment of unsafety" in C++ and other languages and even practical verification can be hard especially when generics get in the way. > In other words, if your rust program has any module in any dependency that has unsafe code (ie. every rust program), it is potentially unsafe, regardless of the borrow checker (because some code path may invoke a 'safe' function that has not be formally verified to be safe, and results in undefined behaviour despite being safe). "Potentially unsafe" for a very small probability. You don't need formal verification to be convinced that something is safe.
- shadowmint 11y ago
  Are you seriously suggesting rusts memory safety promises are ok if they simply 'kind of probably protect you from memory corruption'? /me shakes head. Time for bed.
  - Manishearth 11y ago
    It's not practical to formally verify everything. We'd get nothing done if that was the case. Rust's memory safety promises can be reasoned about clearly without formal verification (which is an arduous process requiring a team of researchers -- basically what RustBelt is doing). This is enough to be convinced that Rust is protecting you from memory corruption. Formal correctness proofs are valuable, but not necessary to ship software. Also, as others have mentioned, Rust is a strict plus over C++ in formal verification as well since once you've verified a module containing unsafe code, you can forget that it contains unsafe code and use it wherever, and modules with safe code can be used without verification. Once verified, Vec<T> is safe to use however you want as long as it's not used in an unsafe block (if it is, just verify that block or module depending on the context).
ralfj 11y ago
One of the fundamental differences is that in Rust, you only have to prove correct every module that contains unsafe code, and the proof then automatically expands to your entire program. The experience in practice is that most module - the ones that are "higher up" in the stack of abstraction - do not need unsafe code, and hence they are automatically safe. If someone proves the Rust libstd correct, and you write a Rust program using only libstd that does not contain unsafe, then your code is guaranteed to be safe. If someone proves the C++ libstd correct, and you write a program using only the C++ libstd - you still have to prove your code correct. Rust provides safe encapsulation, C++ does not.
pcwalton 11y ago
> How is that any improvement on any other language? In Rust, outside of the std::vec module, unless you type "unsafe" there is no way to corrupt a vector that you have. In C++, that's quite easy: undefined behavior can corrupt anything, private fields or not.

Jweb_Guru 11y ago

> How is that any improvement on any other language? Rust provides more facilities for exposing efficient, safe interfaces to unsafe code than do many other languages. The existence of safe and unsafe are not particularly interesting by themselves.

shadowmint 11y ago
Perhaps... but if you have to formally verify the entire module, those facilities aren't doing much good are they?
- Jweb_Guru 11y ago
  You don't have to formally verify the entire module. The module "just" has to be correct :P. Additionally, very often, unsafe code is used in ways that cannot contaminate the entire module (that's the ideal, in fact), and the module that the unsafe code is used in is made deliberately small.

dbaupp 11y ago

I'm not really sure what the problem is here: having to formally verify a module doesn't seem fundamentally different to formally verify a single function. I mean, sure, it's some more code, but there's still well-defined containment. And, being "allowed" to reason about a whole module (well, usually one just cares about a whole type, but these often match, especially for unsafe code) seems far more useful: one can build far more interesting abstractions. If one was forced to reason about a single function at a time, Vec couldn't exist in a useful way, as every function would have to assume the incoming Vec value could be arbitrarily invalid. In any case, there are many many modules with no `unsafe` code, e.g. std::option has none [1], iron::response has none [2], image::jpeg has none [3] (just some random examples). These are automatically safe, if you assume that that the code they call is safe, which seems to me like the only assumption that can make sense: if the safe modules call unsafe ones that aren't safe... well, the problem is in the unsafe ones, not the safe ones. What I'm trying to say is this paragraph doesn't seem to change anything fundamental about the objections to safe vs. unsafe you sometimes write about; it is not introducing anything new, and so the refutations you often receive still apply. [1]: https://github.com/rust-lang/rust/blob/dfaddb732ced1da9d310990df095ca36f43fbc3d/src/libcore/option.rs https://github.com/rust-lang/rust/blob/dfaddb732ced1da9d3109... [2]: https://github.com/iron/iron/blob/d3942d72e3178e7b34ebf1ea0e07b2dc3f9749ee/src/response.rs https://github.com/iron/iron/blob/d3942d72e3178e7b34ebf1ea0e... [3]: https://github.com/PistonDevelopers/image/tree/f2b86c1ec6d3c02b827190671ea9302716e86028/src/jpeg https://github.com/PistonDevelopers/image/tree/f2b86c1ec6d3c...

shadowmint 11y ago
Well, given the most common refute of my concerns is 'you just have to make sure your unsafe blocks are verified to be correct', and the point of this article, is explicitly that this isnt the case... Now its that you have to just make sure all your code is correct, not just the unsafe blocks. /me shrugs I think thats lame, and breaks the promises rust is trying to make about writing safe secure software. If safe code may not be safe, whats the point of it at all. You, are of course welcome to your own oppinion.
- kibwen 11y ago

Manishearth 11y ago

It seems like you're assuming the post is saying that you need formal verification to write safe Rust? I don't think that's the case. Note that the blog post is explicitly in the context of formally verifying Rust and its stdlib. This is not something that's necessary for a "good enough" guarantee that stuff works and is safe. The conclusion you can make is that formally verifying Rust is just as hard as C++ (I'm not sure I agree with this either, but it's really irrelevant), but this doesn't make Rust a worthless language since formal verification is not what you care about for everyday safety guarantees. > If the burden of 'safety' is formal proof of the entire module, then you're (surely) no better off than using C++ and doing exactly the same thing. Well, formal verification is nice, but it's not necessary. Take the Vec<T> interface for example. There are a couple of unsafe methods in it, and the invariant "len is always a valid length". It's easy to check if len is being modified elsewhere. It's easy to reason about these invariants. And it's easy to reason that it upholds the invariants that Rust expects for safe functions. Formal verification is harder, but practical verification is easier since it's contained in a small surface area. On the other hand, there's no "containment of unsafety" in C++ and other languages and even practical verification can be hard especially when generics get in the way. > In other words, if your rust program has any module in any dependency that has unsafe code (ie. every rust program), it is potentially unsafe, regardless of the borrow checker (because some code path may invoke a 'safe' function that has not be formally verified to be safe, and results in undefined behaviour despite being safe). "Potentially unsafe" for a very small probability. You don't need formal verification to be convinced that something is safe.

shadowmint 11y ago
Are you seriously suggesting rusts memory safety promises are ok if they simply 'kind of probably protect you from memory corruption'? /me shakes head. Time for bed.
- Manishearth 11y ago
  It's not practical to formally verify everything. We'd get nothing done if that was the case. Rust's memory safety promises can be reasoned about clearly without formal verification (which is an arduous process requiring a team of researchers -- basically what RustBelt is doing). This is enough to be convinced that Rust is protecting you from memory corruption. Formal correctness proofs are valuable, but not necessary to ship software. Also, as others have mentioned, Rust is a strict plus over C++ in formal verification as well since once you've verified a module containing unsafe code, you can forget that it contains unsafe code and use it wherever, and modules with safe code can be used without verification. Once verified, Vec<T> is safe to use however you want as long as it's not used in an unsafe block (if it is, just verify that block or module depending on the context).

ralfj 11y ago

One of the fundamental differences is that in Rust, you only have to prove correct every module that contains unsafe code, and the proof then automatically expands to your entire program. The experience in practice is that most module - the ones that are "higher up" in the stack of abstraction - do not need unsafe code, and hence they are automatically safe. If someone proves the Rust libstd correct, and you write a Rust program using only libstd that does not contain unsafe, then your code is guaranteed to be safe. If someone proves the C++ libstd correct, and you write a program using only the C++ libstd - you still have to prove your code correct. Rust provides safe encapsulation, C++ does not.

pcwalton 11y ago

> How is that any improvement on any other language? In Rust, outside of the std::vec module, unless you type "unsafe" there is no way to corrupt a vector that you have. In C++, that's quite easy: undefined behavior can corrupt anything, private fields or not.