4 ms·

The question is if this should be done at the language-level or library-level. With sufficient metaprogramming capabilities, an enterprising programmer could wr

The question is if this should be done at the language-level or library-level. With sufficient metaprogramming capabilities, an enterprising programmer could write safe resource management abstractions for Zig. However, this wouldn't make the language "safe by default," which seems to be what Rust programmers are bringing with this criticism. Even if Zig doesn't bring safety by default to the language, however, I think you could get it in practice by making the standard library enforce safety. Then, unless someone goes out of their way to write their own libraries from scratch and eschew all of the safety mechanisms, they would likely live in this safety bubble.

pcwalton 5y ago
Can you write a borrow checker that enforces alias-xor-mut using metaprogramming? I'm skeptical, because of the flow sensitivity you really want to make it practical.
- smasher164 5y ago
  Not sure, but I became optimistic of there being some solution after I saw someone implement affine typing using stateful template metaprogramming: https://godbolt.org/z/PnPPrnPjY https://godbolt.org/z/PnPPrnPjY.
  - pcwalton 5y ago
    That's neat, but also flow-insensitive (and wow, generating a definition for every single use of a variable can't be good for compile-time memory usage).
    - smasher164 5y ago
      Yeah, I'm unaware of any push to bring flow-sensitive typing, or a mechanism that affords flow-sensitive analysis, to Zig.
- pron 5y ago
  You could with some changes to the type capabilities, but I don't think that's the right direction. The main question is do we want soundness or not? This is a general question for various correctness properties, and, at least in the formal methods space, the answer seems to be "not always." Soundness has a cost, and stopping 100% of UAF bugs for the cost of making the language more complex and even adding a few bugs of other kinds, might not be worth it if you can stop 99% of them for a fraction of the cost. I think the goal should be to not have soundness -- IMO it has more downsides than upsides in this case -- and make good runtime detection joined with fast compile/test cycle and even automatic test generation.
  - pcwalton 5y ago
    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.

pcwalton 5y ago

Can you write a borrow checker that enforces alias-xor-mut using metaprogramming? I'm skeptical, because of the flow sensitivity you really want to make it practical.

smasher164 5y ago
Not sure, but I became optimistic of there being some solution after I saw someone implement affine typing using stateful template metaprogramming: https://godbolt.org/z/PnPPrnPjY https://godbolt.org/z/PnPPrnPjY.
- pcwalton 5y ago
  That's neat, but also flow-insensitive (and wow, generating a definition for every single use of a variable can't be good for compile-time memory usage).
  - smasher164 5y ago
    Yeah, I'm unaware of any push to bring flow-sensitive typing, or a mechanism that affords flow-sensitive analysis, to Zig.
pron 5y ago
You could with some changes to the type capabilities, but I don't think that's the right direction. The main question is do we want soundness or not? This is a general question for various correctness properties, and, at least in the formal methods space, the answer seems to be "not always." Soundness has a cost, and stopping 100% of UAF bugs for the cost of making the language more complex and even adding a few bugs of other kinds, might not be worth it if you can stop 99% of them for a fraction of the cost. I think the goal should be to not have soundness -- IMO it has more downsides than upsides in this case -- and make good runtime detection joined with fast compile/test cycle and even automatic test generation.
- pcwalton 5y ago
  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.