5 ms·

The point is that if the unsafe code is correct, any assumptions it is making need to be in the module. Ergo, you should only have to scan the module itself to

The point is that if the unsafe code is correct, any assumptions it is making need to be in the module. Ergo, you should only have to scan the module itself to figure out whether the code is unsafe or not, because if you can't prove safeness by looking at the module it's ipso facto not safe.

steveklabnik 9y ago
Yes, that's what I'm getting at. For more on this: https://doc.rust-lang.org/nomicon/working-with-unsafe.html https://doc.rust-lang.org/nomicon/working-with-unsafe.html
foldr 9y ago
Ok, but then that is true in any language that allows unsafe code. You can also put raw pointer manipulation in a module in C++ code. I do think the significance of Rust's unsafe keyword is exaggerated sometimes. It is just a bit of linting automatically provided by the compiler. Block scoping and tagging of unsafe code doesn't in itself add any guarantees. It's only barely more useful than a simple comment saying "beware: unsafe code here".
- lomnakkus 9y ago
  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.

steveklabnik 9y ago

Yes, that's what I'm getting at. For more on this: https://doc.rust-lang.org/nomicon/working-with-unsafe.html https://doc.rust-lang.org/nomicon/working-with-unsafe.html

foldr 9y ago

Ok, but then that is true in any language that allows unsafe code. You can also put raw pointer manipulation in a module in C++ code. I do think the significance of Rust's unsafe keyword is exaggerated sometimes. It is just a bit of linting automatically provided by the compiler. Block scoping and tagging of unsafe code doesn't in itself add any guarantees. It's only barely more useful than a simple comment saying "beware: unsafe code here".

lomnakkus 9y ago
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.