5 ms·

>> cannot really be expressed in terms of rust's ownership system > Of course it can You cannot share objects using rust's ownership system. Interior mutabil

>> cannot really be expressed in terms of rust's ownership system > Of course it can You cannot share objects using rust's ownership system. Interior mutability involves an unacceptable performance hit (and doesn't actually allow you to share anything). And if you use shared indices into a centralized array, then you have blinded the ownership system, creating pointers that it cannot make sense of. >> This function is not locally correct; in a vacuum, it is impossible to say whether this function violates invariants. > That is also a use-case for unsafe: an unsafe function is one for which the caller is responsible for checking invariants. That's exactly right, and was my thesis; rust's type system does not allow you to prove the correctness of such a function, because it is neither correct nor incorrect without context. 'Unsafe', as a subversion of the type system which allows unsound behaviour, is completely uninteresting wrt the topic at hand; the comparison is a purely theoretical one between non-'unsafe' rust—that is, rust's ownership model—and c.

steveklabnik 5y ago
Interior mutability does not have uniform performance characteristics, Cell has a very different cost (that is, none) over RefCell (which involves checking a flag when accessing). Etc etc. Unsafe does not allow unsound behavior, or rather, it lets you write unsound behavior but that is a bug. You still have to uphold various invariants in unsafe code. It’s there for when you know you can, but the compiler cannot, which is an inherent property of any sound system.
- moonchild 5y ago
  > Unsafe does not allow unsound behavior, or rather, it lets you write unsound behavior but that is a bug. You still have to uphold various invariants in unsafe code. It’s there for when you know you can, but the compiler cannot, which is an inherent property of any sound system. I don't understand what you're saying here. Rust-without-'unsafe' is a sound language; i.e. any program which types will be unable to violate runtime invariants. Rust-with-'unsafe' is an unsound language; i.e. there are programs which type but yet violate runtime invariants. That is a bug in those programs—sure, yes, of course. It is not a bug in rust; it is the language functioning as intended. However the topic at hand is the relationship between rust's type system and c's; hence unsafe is completely uninteresting, because it is a tool for subverting rust's type system. (It occurs to me now that I might have gotten a less generally defensive response had I made the original comparison between rust and a hypothetical rust without unsafe. Oh well)
  - steveklabnik 5y ago
    > However the topic at hand is the relationship between rust's type system and c's; hence unsafe is completely uninteresting, Gotcha, I was just trying to clarify the semantics of unsafe, lots of people think it suddenly lets you do whatever you want, and while it will let you, that doesn't mean that you can, which is an important distinction. You're right that this puts it in the same general category of C in a theoretical perspective, I think practice will bear out that it's not a binary proposition, but time will tell :)
    - infogulch 5y ago
      If manually managing memory is like wielding a gun, the borrow checker is an automatic safety that prevents you from pulling the trigger when you're roughly pointing it at yourself. But it's coarse-grained and errs on the side of caution; it simulates your foot as as the rectangular box that would contain it, not as a detailed 3D mesh. If you really think you can aim it between your toes and avoid hitting yourself (for example, "the value returned by this function must remain alive for no more than 15 successive invocations of this function"), unsafe will let you try, but the borrow checker's built-in rules isn't granular enough to help you, though it will still stop you if you accidentally put your hand in front without declaring it. C is like a laser gun in a room full of oddly-shaped mirrors with no safety at all. Good luck.
      - moonchild 5y ago
        > it's coarse-grained and errs on the side of caution That's what type systems in general do. There is no type system for a turing-complete language that is both sound and complete. (Trivial proof: if (undecidable) halt; unsound.)
littlestymaar 5y ago
> That's exactly right, and was my thesis; rust's type system does not allow you to prove the correctness of such a function, because it is neither correct nor incorrect without context. 'Unsafe', as a subversion of the type system which allows unsound behavior, is completely uninteresting wrt the topic at hand; For the record, the “topic at hand” was the memory model not the type-system, nor the theorem proving capabilities of the borrow checker. Your arguments are not wrong per se, but they are completely missing the topic.

steveklabnik 5y ago

Interior mutability does not have uniform performance characteristics, Cell has a very different cost (that is, none) over RefCell (which involves checking a flag when accessing). Etc etc. Unsafe does not allow unsound behavior, or rather, it lets you write unsound behavior but that is a bug. You still have to uphold various invariants in unsafe code. It’s there for when you know you can, but the compiler cannot, which is an inherent property of any sound system.

moonchild 5y ago
> Unsafe does not allow unsound behavior, or rather, it lets you write unsound behavior but that is a bug. You still have to uphold various invariants in unsafe code. It’s there for when you know you can, but the compiler cannot, which is an inherent property of any sound system. I don't understand what you're saying here. Rust-without-'unsafe' is a sound language; i.e. any program which types will be unable to violate runtime invariants. Rust-with-'unsafe' is an unsound language; i.e. there are programs which type but yet violate runtime invariants. That is a bug in those programs—sure, yes, of course. It is not a bug in rust; it is the language functioning as intended. However the topic at hand is the relationship between rust's type system and c's; hence unsafe is completely uninteresting, because it is a tool for subverting rust's type system. (It occurs to me now that I might have gotten a less generally defensive response had I made the original comparison between rust and a hypothetical rust without unsafe. Oh well)
- steveklabnik 5y ago
  > However the topic at hand is the relationship between rust's type system and c's; hence unsafe is completely uninteresting, Gotcha, I was just trying to clarify the semantics of unsafe, lots of people think it suddenly lets you do whatever you want, and while it will let you, that doesn't mean that you can, which is an important distinction. You're right that this puts it in the same general category of C in a theoretical perspective, I think practice will bear out that it's not a binary proposition, but time will tell :)
  - infogulch 5y ago
    If manually managing memory is like wielding a gun, the borrow checker is an automatic safety that prevents you from pulling the trigger when you're roughly pointing it at yourself. But it's coarse-grained and errs on the side of caution; it simulates your foot as as the rectangular box that would contain it, not as a detailed 3D mesh. If you really think you can aim it between your toes and avoid hitting yourself (for example, "the value returned by this function must remain alive for no more than 15 successive invocations of this function"), unsafe will let you try, but the borrow checker's built-in rules isn't granular enough to help you, though it will still stop you if you accidentally put your hand in front without declaring it. C is like a laser gun in a room full of oddly-shaped mirrors with no safety at all. Good luck.
    - moonchild 5y ago
      > it's coarse-grained and errs on the side of caution That's what type systems in general do. There is no type system for a turing-complete language that is both sound and complete. (Trivial proof: if (undecidable) halt; unsound.)

littlestymaar 5y ago

> That's exactly right, and was my thesis; rust's type system does not allow you to prove the correctness of such a function, because it is neither correct nor incorrect without context. 'Unsafe', as a subversion of the type system which allows unsound behavior, is completely uninteresting wrt the topic at hand; For the record, the “topic at hand” was the memory model not the type-system, nor the theorem proving capabilities of the borrow checker. Your arguments are not wrong per se, but they are completely missing the topic.