5 ms·

The point isn't to tag the unsafe code. The point is that code NOT bearing the tag is guaranteed to be memory safe and free of race conditions. It's like havin

The point isn't to tag the unsafe code. The point is that code NOT bearing the tag is guaranteed to be memory safe and free of race conditions. It's like having a Trusted Computing Base which is very small, verifying the hell out that TCB and then relying on its invariants when building up the rest of the system. C++ cannot do this at present because all code must by definition be treated as untrusted/unsafe. In Rust you simply don't have access to do e.g. pointer arithmetic in safe code and that code is kept separate from unsafe code by the compiler. (Modulo compiler bugs, etc.)

foldr 9y ago
>The point is that code NOT bearing the tag is guaranteed to be memory safe and free of race conditions. No, it isn't, because it may call code that uses unsafe constructs. (That's why you don't have to put an unsafe block around your code every time you push a value into a vector.) >C++ cannot do this at present because all code must by definition be treated as untrusted/unsafe. No, only the code that uses unsafe constructs needs to be treated as unsafe. You could easily make a tool that automatically inserted 'unsafe' tags around C++ code that used unsafe constructs such as pointer arithmetic. The fact that this tool is built into the Rust compiler is just a convenience.
- Jweb_Guru 9y ago
  > No, it isn't, because it may call code that uses unsafe constructs. (That's why you don't have to put an unsafe block around your code every time you push a value into a vector.) For the last time: if you have proven the module using the unsafe code correct, you do not have to treat code calling it as unsafe, and safe code calling it is guaranteed to be free of data races and memory safe. > No, only the code that uses unsafe constructs needs to be treated as unsafe. You could easily make a tool that automatically inserted 'unsafe' tags around C++ code that used unsafe constructs such as pointer arithmetic. The fact that this tool is built into the Rust compiler is just a convenience. That wouldn't solve anything at all. C++'s type system cannot and does not enforce safe usage of APIs like string_view; it doesn't matter whether the safe code is using "unsafe constructs." If you choose to mark all C++ or C libraries that rely on invariants that can't be proven safe by the type system as unsafe, you will quickly find that essentially your entire program is covered in an unsafe block. The difference in Rust is not that it has unsafe blocks, but that its type system can safely encapsulate interesting APIs whose proof of safety is nontrivial.
  - foldr 9y ago
    > if you have proven the module using the unsafe code correct, you do not have to treat code calling it as unsafe Yes, I know, but lomnakkus said "code NOT bearing the [unsafe] tag is guaranteed to be memory safe" without adding this qualification. Without the qualification, the statement is incorrect. >The difference in Rust is not that it has unsafe blocks Indeed. That’s what I said above. For some reason, Rust advocates don't like it when people point out that unsafe blocks, in and of themselves, do not add any kind of safety guarantees to the language or limit the effects of unsafe code. Of course Rust's type system is able to express important invariants that C++'s type system can't, and this can be used to prevent iterator invalidation etc. etc. The point is that if you do have an unsafe block in your own code, you are going to have to go to the trouble of constructing a formal proof -- using tools that haven't been fully developed yet -- in order to be sure that any of the rest of your code is safe. And at present, the proof requires a translation step, which cannot be formally specified, from Rust code to LambdaRust code. Rust is undoubtably much safer than C++ in practice. I just think the extent to which it provides hard and fast safety guarantees tends to be exaggerated somewhat in its marketing.
    - Jweb_Guru 9y ago
      Sure. There is a lot of work left to do to bridge the gap between the formal model and Rust code. But we can be reasonably confident at this point that the libraries we've proven correct actually are correct (modulo translation errors), and we specifically set out to prove things about libraries that were safe for interesting or nontrivial reasons. That's a huge step forward. It means that, with some time and effort, producing codebases with formal proofs of memory safety can be done at quite low verification cost. The executable might need to be generated with something other than LLVM, of course, but using tools like CompCert is possible in these cases; the primary difficulty with it is normally that it only correctly compiles correct C, which is difficult to find in the wild to say the least. Not only that, but thanks to Rust's type system being able to express separation logic invariants, we may be able to do many functional proofs of correctness more easily; right now, refinement types are mostly limited to systems like Liquid Haskell because it is hard to generate invariants for impure code, but by integrating with Rust's type system such things become possible. There is at least one research group currently investigating this possibility, and it looks quite promising. Such work entirely depends on the fact that safe code that passes the borrow checker must be memory safe and has enough annotations that resource aliasing can be determined statically, freeing programmers from the burden of manually specifying primitives like separating conjunction and magic wand. Invariants would be stated at the function level and verified modularly (on a function by function basis), rather than current state of the art techniques used by model checkers, which usually require whole program verification. This has the chance to put scalable formal verification of functional correctness for many common errors (like integer overflow and out of bounds array accesses) in the hands of programmers who don't have training in formal verification; I find that very exciting! I'd also add: requiring the keyword unsafe actually is fairly important in practice. Without it, there wouldn't be a way to assert to the compiler when a block of code that used unsafe primitives was safe (I suppose you could use something like "trusted" to mark a block safe instead of "unsafe" to mark it unsafe, but I suspect the ergonomics of that would be fairly untenable). So it's not entirely right to say that unsafe is pointless; it's a necessary component. It's just a trivial one.

foldr 9y ago

>The point is that code NOT bearing the tag is guaranteed to be memory safe and free of race conditions. No, it isn't, because it may call code that uses unsafe constructs. (That's why you don't have to put an unsafe block around your code every time you push a value into a vector.) >C++ cannot do this at present because all code must by definition be treated as untrusted/unsafe. No, only the code that uses unsafe constructs needs to be treated as unsafe. You could easily make a tool that automatically inserted 'unsafe' tags around C++ code that used unsafe constructs such as pointer arithmetic. The fact that this tool is built into the Rust compiler is just a convenience.

Jweb_Guru 9y ago
> No, it isn't, because it may call code that uses unsafe constructs. (That's why you don't have to put an unsafe block around your code every time you push a value into a vector.) For the last time: if you have proven the module using the unsafe code correct, you do not have to treat code calling it as unsafe, and safe code calling it is guaranteed to be free of data races and memory safe. > No, only the code that uses unsafe constructs needs to be treated as unsafe. You could easily make a tool that automatically inserted 'unsafe' tags around C++ code that used unsafe constructs such as pointer arithmetic. The fact that this tool is built into the Rust compiler is just a convenience. That wouldn't solve anything at all. C++'s type system cannot and does not enforce safe usage of APIs like string_view; it doesn't matter whether the safe code is using "unsafe constructs." If you choose to mark all C++ or C libraries that rely on invariants that can't be proven safe by the type system as unsafe, you will quickly find that essentially your entire program is covered in an unsafe block. The difference in Rust is not that it has unsafe blocks, but that its type system can safely encapsulate interesting APIs whose proof of safety is nontrivial.
- foldr 9y ago
  > if you have proven the module using the unsafe code correct, you do not have to treat code calling it as unsafe Yes, I know, but lomnakkus said "code NOT bearing the [unsafe] tag is guaranteed to be memory safe" without adding this qualification. Without the qualification, the statement is incorrect. >The difference in Rust is not that it has unsafe blocks Indeed. That’s what I said above. For some reason, Rust advocates don't like it when people point out that unsafe blocks, in and of themselves, do not add any kind of safety guarantees to the language or limit the effects of unsafe code. Of course Rust's type system is able to express important invariants that C++'s type system can't, and this can be used to prevent iterator invalidation etc. etc. The point is that if you do have an unsafe block in your own code, you are going to have to go to the trouble of constructing a formal proof -- using tools that haven't been fully developed yet -- in order to be sure that any of the rest of your code is safe. And at present, the proof requires a translation step, which cannot be formally specified, from Rust code to LambdaRust code. Rust is undoubtably much safer than C++ in practice. I just think the extent to which it provides hard and fast safety guarantees tends to be exaggerated somewhat in its marketing.
  - Jweb_Guru 9y ago
    Sure. There is a lot of work left to do to bridge the gap between the formal model and Rust code. But we can be reasonably confident at this point that the libraries we've proven correct actually are correct (modulo translation errors), and we specifically set out to prove things about libraries that were safe for interesting or nontrivial reasons. That's a huge step forward. It means that, with some time and effort, producing codebases with formal proofs of memory safety can be done at quite low verification cost. The executable might need to be generated with something other than LLVM, of course, but using tools like CompCert is possible in these cases; the primary difficulty with it is normally that it only correctly compiles correct C, which is difficult to find in the wild to say the least. Not only that, but thanks to Rust's type system being able to express separation logic invariants, we may be able to do many functional proofs of correctness more easily; right now, refinement types are mostly limited to systems like Liquid Haskell because it is hard to generate invariants for impure code, but by integrating with Rust's type system such things become possible. There is at least one research group currently investigating this possibility, and it looks quite promising. Such work entirely depends on the fact that safe code that passes the borrow checker must be memory safe and has enough annotations that resource aliasing can be determined statically, freeing programmers from the burden of manually specifying primitives like separating conjunction and magic wand. Invariants would be stated at the function level and verified modularly (on a function by function basis), rather than current state of the art techniques used by model checkers, which usually require whole program verification. This has the chance to put scalable formal verification of functional correctness for many common errors (like integer overflow and out of bounds array accesses) in the hands of programmers who don't have training in formal verification; I find that very exciting! I'd also add: requiring the keyword unsafe actually is fairly important in practice. Without it, there wouldn't be a way to assert to the compiler when a block of code that used unsafe primitives was safe (I suppose you could use something like "trusted" to mark a block safe instead of "unsafe" to mark it unsafe, but I suspect the ergonomics of that would be fairly untenable). So it's not entirely right to say that unsafe is pointless; it's a necessary component. It's just a trivial one.