3 ms·

> There is simply no justification to make that equivalence. I explained in some detail exactly why this equivalence exists. I actually have a small hope that

> There is simply no justification to make that equivalence. I explained in some detail exactly why this equivalence exists. I actually have a small hope that this time there are enough people who think it's a bad idea that we don't have to watch this play out for decades before the realisation as we did with C and C++. Yes it's exactly Rice's Theorem, it's that simple and that drastic. You can choose what to do when you're not sure, but you can't choose (no matter how much effort you imagine applying) to always be sure†, that Undecidability is what Henry Rice proved. The languages you mention choose to treat "not sure" the same as "nope", like Rust does, you apparently prefer languages like Zig or C++ which instead treat "not sure" as "it's fine". I have explained why that's a terrible idea already. The underlying fault, which is why I'm confident this reproduces, is in humans. To err is human. We are going to make mistakes and under the Rust model we will curse, perhaps blame the compiler, or the machine, and fix our mistake. In C++ or Zig our mistake compiles just fine and now the software is worse. † For general purpose languages. One clever trick here is that you can just not be a general purpose language. Trivial semantic properties are easily decided, so if your language can make the desired properties trivial then there's no checking and Rice's Theorem doesn't apply. The easy example is, if my language has no looping type features, no recursive calls, nothing like that, all its programs trivially halt - a property we obviously can't decidably check in a general purpose language.

pron 1y ago
> I explained in some detail exactly why this equivalence exists. No, you assumed that Zig and C++ are equivalent and concluded that they'll follow a similar trajectory. It's your premise that's unjustified. A problem you'd have to contend with is that Rust is much more similar to C++ than Zig in multiple respects, which may matter more or less than the level of safety when predicting the language trajectory. > But you can't choose (no matter how much effort you imagine applying) to always be sure That is not Rice's theorem. You can certainly choose to prove every program correct. What you cannot do is have a general mechanism that would prove all programs in a certain language correct. > One clever trick here is that you can just not be a general purpose language. That's not so much a clever trick as the core of all simple (i.e. non-dependent) type systems. Type-safety in those languages then trivially implies some property, which is an inductive invariant (or composable invariant) that's stronger than some desired property. E.g. in Rust, "borrow/lifetime-safety" is stronger than UAF-safety. However, because an effort to prove any property must exist, we can find it for some language that trivially offers it by looking at the cost of translating a correct program in some other language that doesn't guarantee the property to one that does. The reason why it's more of a theoretical point than a practical one is because it could be reasonably argued that writing a memory-safety program in C is harder than doing it in Rust in the first place, but either way, there's some effort there that isn't there when writing the program in, say, Java.
- akkad33 1y ago
  > No, you assumed that Zig and C++ are equivalent and concluded that they'll follow a similar trajectory. It's your premise that's unjustified. They did not say Zig and C++ are equivalent
uecker 1y ago
And yet, in reality, Rust is also on the "if I am not sure I simply attest that it is fine" side on the fence.
- ViewTrick1002 1y ago
  Which is why there is an effort to formally verify the unsafe use in the Rust standard library. I would also say that unsafe causes a very different human reaction. When like Zig, C or C++ everything is potentially unsafe then you can't scrutinize everything. When submitting a PR in Rust containing unsafe code everyone wants to understand what happens because it is both rare, and everyone are cautious about the dangers posed. The first question on everyone's mind always is: Does this need unsafe?
  - pron 1y ago
    > When like Zig, C or C++ everything is potentially unsafe It is not true that in Zig "everything is potentially unsafe". Zig offers bounds safety, which, BTW, eliminates the most dangerous kind of memory unsafety (https://cwe.mitre.org/top25/archive/2024/2024_cwe_top25.html https://cwe.mitre.org/top25/archive/2024/2024_cwe_top25.html).
    - tialaramex 1y ago
      Suppose I have a self-contained Zig project and it has a nasty memory safety bug - how can I identify where the cause might be? What parts of my project source are potentially unsafe ? You've said it's not everything, so, what's excluded? What can I rule out?
      - pron 1y ago
        You can rule out a bounds violations from all but specifically marked unsafe code.
        ViewTrick1002 1y ago

pron 1y ago

> I explained in some detail exactly why this equivalence exists. No, you assumed that Zig and C++ are equivalent and concluded that they'll follow a similar trajectory. It's your premise that's unjustified. A problem you'd have to contend with is that Rust is much more similar to C++ than Zig in multiple respects, which may matter more or less than the level of safety when predicting the language trajectory. > But you can't choose (no matter how much effort you imagine applying) to always be sure That is not Rice's theorem. You can certainly choose to prove every program correct. What you cannot do is have a general mechanism that would prove all programs in a certain language correct. > One clever trick here is that you can just not be a general purpose language. That's not so much a clever trick as the core of all simple (i.e. non-dependent) type systems. Type-safety in those languages then trivially implies some property, which is an inductive invariant (or composable invariant) that's stronger than some desired property. E.g. in Rust, "borrow/lifetime-safety" is stronger than UAF-safety. However, because an effort to prove any property must exist, we can find it for some language that trivially offers it by looking at the cost of translating a correct program in some other language that doesn't guarantee the property to one that does. The reason why it's more of a theoretical point than a practical one is because it could be reasonably argued that writing a memory-safety program in C is harder than doing it in Rust in the first place, but either way, there's some effort there that isn't there when writing the program in, say, Java.

akkad33 1y ago
> No, you assumed that Zig and C++ are equivalent and concluded that they'll follow a similar trajectory. It's your premise that's unjustified. They did not say Zig and C++ are equivalent

uecker 1y ago

And yet, in reality, Rust is also on the "if I am not sure I simply attest that it is fine" side on the fence.

ViewTrick1002 1y ago
Which is why there is an effort to formally verify the unsafe use in the Rust standard library. I would also say that unsafe causes a very different human reaction. When like Zig, C or C++ everything is potentially unsafe then you can't scrutinize everything. When submitting a PR in Rust containing unsafe code everyone wants to understand what happens because it is both rare, and everyone are cautious about the dangers posed. The first question on everyone's mind always is: Does this need unsafe?
- pron 1y ago
  > When like Zig, C or C++ everything is potentially unsafe It is not true that in Zig "everything is potentially unsafe". Zig offers bounds safety, which, BTW, eliminates the most dangerous kind of memory unsafety (https://cwe.mitre.org/top25/archive/2024/2024_cwe_top25.html https://cwe.mitre.org/top25/archive/2024/2024_cwe_top25.html).
  - tialaramex 1y ago
    Suppose I have a self-contained Zig project and it has a nasty memory safety bug - how can I identify where the cause might be? What parts of my project source are potentially unsafe ? You've said it's not everything, so, what's excluded? What can I rule out?
    - pron 1y ago
      You can rule out a bounds violations from all but specifically marked unsafe code.
      - ViewTrick1002 1y ago