3 ms·

I mean, you're essentially saying here that memory safety is not worth having, which is a position increasingly at odds with the evidence.

pron 5y ago
Not at all. I'm saying that sound guarantees are not the only way to achieve memory safety. The goal isn't to use a language that makes sound guarantees, but to write correct programs (even Rust programs don't give you sound guarantees for memory safety as many of them depend on unsafe code that isn't soundly proven). That the cheapest way to write such programs is to have sound guarantees for everything is an interesting hypothesis, which would get you a language like, say, Idris, but it is not the consensus. There are many paths to safety and correctness, and not all of them go through soundness. I'd venture to say that most properties your life depends on in safety-critical systems are not soundly guaranteed.
- pcwalton 5y ago
  When I say "memory safety" I mean "language-enforced memory safety". You're saying that having the language enforce memory safety isn't worthwhile. > even Rust programs don't give you sound guarantees for memory safety as many of them depend on unsafe code that isn't soundly proven There's no such thing as 100% memory safety; at the extreme end there are bit flips caused by cosmic rays. But the evidence suggests that practical language-enforced memory safety is actually worthwhile, despite the fact that no theoretical absolute memory safety is possible. All memory-safe languages have runtimes and FFIs, which in Rust is the unsafe blocks. This doesn't change the fact that, empirically, memory safety, even the imperfect memory safety we have to live with in the real world, is a meaningful improvement in stability and security. > That the cheapest way to write such programs is to have sound guarantees for everything is an interesting hypothesis, which would get you a language like, say, Idris, but it is not the consensus. Straw man. Nobody is talking about proving all code correct. What is reasonably describable as consensus nowadays is that having the language enforce memory safety is worthwhile. The idea that enforced memory safety has, in your words, "more downsides than upsides", is increasingly at odds with the consensus. To get concrete, I see no reason to believe that quarantine (Zig's current solution to UAF) is a meaningful solution to use-after-free problems, given that quarantine has been deployed for a long time in production allocators in other languages and has failed to eliminate this bug class in the wild.
  - pron 5y ago
    > You're saying that having the language enforce memory safety isn't worthwhile. I am saying that it may come at a cost, and overall it may not be worthwhile; but, of course, there are different kinds of safety bugs, different kinds of soundness, different costs, and different alternatives. > But the evidence suggests that practical language-enforced memory safety is actually worthwhile, despite the fact that no theoretical absolute memory safety is possible What is it that the evidence suggests exactly? There are so many variables. For example, Zig's runtime checking could be much more effective than similar systems for C or C++, because it is much easier to track all pointers in Zig, just as its overflow protection is far more effective than sanitisers in C, because there's no pointer arithmetic (unless using unsafe operations) and all buffer sizes are always known. So you can't compare what Zig can do to what C can do. Then there's the question of what the safety mechanism is. Then, for each point in this coordinate space, what is the fitness you're looking at? Reducing a particular bug or improved overall correctness? > What is reasonably describable as consensus nowadays is that having the language enforce memory safety is worthwhile. No, this is not true, or at least, that depends on what is the fitness function and what exactly it is compared against. To put it bluntly, there is absolutely no consensus that Rust would more cheaply produce programs that are more correct overall than Zig. It's possible this is the case, as is the opposite or that the two are about the same, but we just don't know yet. > To get concrete, I see no reason to believe that quarantine (Zig's current solution to UAF) is a meaningful solution to use-after-free problems, given that quarantine has been deployed for a long time in production allocators in other languages and has failed to eliminate this bug class in the wild. But that's not how we look at correctness. The goal isn't to eliminate all UAF bugs. Of course completely (or close to it) eliminating a specific bug is more effective at reducing it than not completely eliminating it. If my only goal was to eliminate UAF, then I'd choose Rust's approach over Zig's. But usually our goal is to write a program that meets our correctness level for all bugs combined in the cheapest way possible. Investing a huge language complexity budget in completely eliminating UAF, as opposed to, say, reducing it by 99%, has not been shown to be the best way to achieve what we actually want. I am not saying that it's not reasonable to believe that soundly eliminating this particular bug with something like Rust's ownership and lifetime system ends up being better overall, but it is equally reasonable, based on what we know, to believe that Zig's way is more effective overall, or that the two end up the same. There's just so much we don't know about correctness.

pron 5y ago

Not at all. I'm saying that sound guarantees are not the only way to achieve memory safety. The goal isn't to use a language that makes sound guarantees, but to write correct programs (even Rust programs don't give you sound guarantees for memory safety as many of them depend on unsafe code that isn't soundly proven). That the cheapest way to write such programs is to have sound guarantees for everything is an interesting hypothesis, which would get you a language like, say, Idris, but it is not the consensus. There are many paths to safety and correctness, and not all of them go through soundness. I'd venture to say that most properties your life depends on in safety-critical systems are not soundly guaranteed.

pcwalton 5y ago
When I say "memory safety" I mean "language-enforced memory safety". You're saying that having the language enforce memory safety isn't worthwhile. > even Rust programs don't give you sound guarantees for memory safety as many of them depend on unsafe code that isn't soundly proven There's no such thing as 100% memory safety; at the extreme end there are bit flips caused by cosmic rays. But the evidence suggests that practical language-enforced memory safety is actually worthwhile, despite the fact that no theoretical absolute memory safety is possible. All memory-safe languages have runtimes and FFIs, which in Rust is the unsafe blocks. This doesn't change the fact that, empirically, memory safety, even the imperfect memory safety we have to live with in the real world, is a meaningful improvement in stability and security. > That the cheapest way to write such programs is to have sound guarantees for everything is an interesting hypothesis, which would get you a language like, say, Idris, but it is not the consensus. Straw man. Nobody is talking about proving all code correct. What is reasonably describable as consensus nowadays is that having the language enforce memory safety is worthwhile. The idea that enforced memory safety has, in your words, "more downsides than upsides", is increasingly at odds with the consensus. To get concrete, I see no reason to believe that quarantine (Zig's current solution to UAF) is a meaningful solution to use-after-free problems, given that quarantine has been deployed for a long time in production allocators in other languages and has failed to eliminate this bug class in the wild.
- pron 5y ago
  > You're saying that having the language enforce memory safety isn't worthwhile. I am saying that it may come at a cost, and overall it may not be worthwhile; but, of course, there are different kinds of safety bugs, different kinds of soundness, different costs, and different alternatives. > But the evidence suggests that practical language-enforced memory safety is actually worthwhile, despite the fact that no theoretical absolute memory safety is possible What is it that the evidence suggests exactly? There are so many variables. For example, Zig's runtime checking could be much more effective than similar systems for C or C++, because it is much easier to track all pointers in Zig, just as its overflow protection is far more effective than sanitisers in C, because there's no pointer arithmetic (unless using unsafe operations) and all buffer sizes are always known. So you can't compare what Zig can do to what C can do. Then there's the question of what the safety mechanism is. Then, for each point in this coordinate space, what is the fitness you're looking at? Reducing a particular bug or improved overall correctness? > What is reasonably describable as consensus nowadays is that having the language enforce memory safety is worthwhile. No, this is not true, or at least, that depends on what is the fitness function and what exactly it is compared against. To put it bluntly, there is absolutely no consensus that Rust would more cheaply produce programs that are more correct overall than Zig. It's possible this is the case, as is the opposite or that the two are about the same, but we just don't know yet. > To get concrete, I see no reason to believe that quarantine (Zig's current solution to UAF) is a meaningful solution to use-after-free problems, given that quarantine has been deployed for a long time in production allocators in other languages and has failed to eliminate this bug class in the wild. But that's not how we look at correctness. The goal isn't to eliminate all UAF bugs. Of course completely (or close to it) eliminating a specific bug is more effective at reducing it than not completely eliminating it. If my only goal was to eliminate UAF, then I'd choose Rust's approach over Zig's. But usually our goal is to write a program that meets our correctness level for all bugs combined in the cheapest way possible. Investing a huge language complexity budget in completely eliminating UAF, as opposed to, say, reducing it by 99%, has not been shown to be the best way to achieve what we actually want. I am not saying that it's not reasonable to believe that soundly eliminating this particular bug with something like Rust's ownership and lifetime system ends up being better overall, but it is equally reasonable, based on what we know, to believe that Zig's way is more effective overall, or that the two end up the same. There's just so much we don't know about correctness.