4 ms·

In addition to what others have already said: "unsafe" just means that the compiler does not understand your data structure well enough to enforce its invariant

In addition to what others have already said: "unsafe" just means that the compiler does not understand your data structure well enough to enforce its invariants. And that's okay! The zen of Rust is not to eliminate unsafe code. That would require a compiler so ludicrously sophisticated that it would be borderline magical. The zen of Rust is to reduce unsafe code to the minimum, to have only 1% or 0.1% of your code that is unsafe and needs to be reviewed extra-super-duper-rigorously.

moonchild 6y ago
> The zen of Rust is not to eliminate unsafe code. That would require a compiler so ludicrously sophisticated that it would be borderline magical I'm not sure what you mean by ‘borderline magical’. There are formal verification tools for e.g. c and a subset of ada. The sel4 microkernel has been completely formally verified; i.e. it has no unsafe code.
- zesterer 6y ago
  There is no one definition of 'formal verification'. Sel4's verification required developers to specifically demarcate the behaviour they desire and generally requires the use of abstractions with very predictable safe semantics. In addition, Sel4 is less than 9k lines of code. That is a very, very long way from developing a general-purpose compiler for a general-purpose system language that can perform arbitrary formal verification for arbitrary code. That's not the goal of Rust and I doubt that it would be a particularly useful one for 99% of developers anyway. The goal of Rust's safety promise is that the verification and review of an entire codebase (as would be the case in C) shrinks down to just a very small corner of that codebase (that which is demarcated as 'unsafe'). In practice, I think that unsafe uses are substantially rarer than that even. Veloren (https://gitlab.com/veloren/veloren/ https://gitlab.com/veloren/veloren/) has almost 120,000 lines of code nowadays and yet has fewer usages of unsafe code than you can count with a single hand.
  - moonchild 6y ago
    > Sel4 is less than 9k lines of code By my count, it's approximately 86k loc. > That is a very, very long way from developing a general-purpose compiler for a general-purpose system language that can perform arbitrary formal verification for arbitrary code Even a language like ATS (which is ‘general-purpose’) can verify a substantial majority of code which would need to be marked ‘unsafe’ under rust. (It also proves a number of other interesting and desirable features, like bounding recursion.) > I doubt that [complete formal verification, as a goal] would be a particularly useful one for 99% of developers anyway Why? I find that a pretty attractive proposition. Safety isn't an end to itself; it's means that enables a broader desire to produce more reliable, correct software. One of the great things that rust (and, to a lesser extent, typescript) have done is to bring more expressive, powerful type systems into vogue. Ones that can more effectively model real-world systems and verify program behaviour. Why choose to stop, arbitrarily, with however much power rust's type system happens to have at the moment? > Veloren (https://gitlab.com/veloren/veloren/ https://gitlab.com/veloren/veloren/) has almost 120,000 lines of code nowadays and yet has fewer usages of unsafe code than you can count with a single hand Veloren is a video game and arguably has no excuse for having any unsafe code. Redox, which is probably a better case study, uses the keyword 8k times.

moonchild 6y ago

> The zen of Rust is not to eliminate unsafe code. That would require a compiler so ludicrously sophisticated that it would be borderline magical I'm not sure what you mean by ‘borderline magical’. There are formal verification tools for e.g. c and a subset of ada. The sel4 microkernel has been completely formally verified; i.e. it has no unsafe code.

zesterer 6y ago
There is no one definition of 'formal verification'. Sel4's verification required developers to specifically demarcate the behaviour they desire and generally requires the use of abstractions with very predictable safe semantics. In addition, Sel4 is less than 9k lines of code. That is a very, very long way from developing a general-purpose compiler for a general-purpose system language that can perform arbitrary formal verification for arbitrary code. That's not the goal of Rust and I doubt that it would be a particularly useful one for 99% of developers anyway. The goal of Rust's safety promise is that the verification and review of an entire codebase (as would be the case in C) shrinks down to just a very small corner of that codebase (that which is demarcated as 'unsafe'). In practice, I think that unsafe uses are substantially rarer than that even. Veloren (https://gitlab.com/veloren/veloren/ https://gitlab.com/veloren/veloren/) has almost 120,000 lines of code nowadays and yet has fewer usages of unsafe code than you can count with a single hand.
- moonchild 6y ago
  > Sel4 is less than 9k lines of code By my count, it's approximately 86k loc. > That is a very, very long way from developing a general-purpose compiler for a general-purpose system language that can perform arbitrary formal verification for arbitrary code Even a language like ATS (which is ‘general-purpose’) can verify a substantial majority of code which would need to be marked ‘unsafe’ under rust. (It also proves a number of other interesting and desirable features, like bounding recursion.) > I doubt that [complete formal verification, as a goal] would be a particularly useful one for 99% of developers anyway Why? I find that a pretty attractive proposition. Safety isn't an end to itself; it's means that enables a broader desire to produce more reliable, correct software. One of the great things that rust (and, to a lesser extent, typescript) have done is to bring more expressive, powerful type systems into vogue. Ones that can more effectively model real-world systems and verify program behaviour. Why choose to stop, arbitrarily, with however much power rust's type system happens to have at the moment? > Veloren (https://gitlab.com/veloren/veloren/ https://gitlab.com/veloren/veloren/) has almost 120,000 lines of code nowadays and yet has fewer usages of unsafe code than you can count with a single hand Veloren is a video game and arguably has no excuse for having any unsafe code. Redox, which is probably a better case study, uses the keyword 8k times.