4 ms·

> It “could”, in the same sense that “vaccine could cause autism” No. The claim "design with tradeoffs X leads to more correct programs than design with tradeo

by pron 4y ago

> It “could”, in the same sense that “vaccine could cause autism” No. The claim "design with tradeoffs X leads to more correct programs than design with tradeoffs Y" is the one that requires evidence. The null hypothesis is that it doesn't. > Interestingly enough, you spend much, much, more time talking about it than himself… As I said, software correctness is my thing. When I saw Zig's brilliant, revolutionary design, I thought, wow, that's a powerful and interesting approach to software correctness. I thought pretty much the same when I saw Rust's design. My aesthetic preferences lean toward simpler languages, just as others' lean toward a more refined type system, but both of these languages make correctness a major focus of their design, they go after it in very different but equally interesting and novel ways, and it will be fascinating to learn which, if any, can achieve better correctness. However, anyone who says we already know is not telling the truth, and probably has a shaky understanding of the subject. > So the gist of your argument is that we don't know No. The reason we don't know is that we don't have evidence one way or another. I gave you one example as an intuition for why your hypothesis might be false. > I was referring to this quote of yours above: “Zig has a pretty good memory safety story”. Which is empirically not so good. You're saying it's not good because it doesn't try to completely eliminate such errors? That's called begging the question. Now, you can say many things about me, but when talking about technical subjects I try pick my words precisely. I'll gladly keep discussing the substance of the matter -- I've devoted a lot to it and I care deeply about it (look at my blog) -- but if you're trying to poke at my words you will most likely waste both our time. Yes, Zig has a pretty good memory safety story. It's a combination of sound spatial safety, precise pointer tracking, as well as some tools, to make catching temporal safety issues easier. It's not only a pretty good story, it's also interesting and rather novel one -- like Rust's -- only its particulars are very different. Zig's memory safety story is not perfect because the cost of perfection, Zig's philosophy believes, is too high, to the point of working against the goal of correctness. There are two relevant open questions: If correctness is all you care about, what price should you pay for memory safety? And what if you also care about other things? I don't know the answer to these questions -- nobody does -- but we need both Zig and Rust to help us learn.

littlestymaar 4y ago
> No. The claim "design with tradeoffs X leads to more correct programs than design with tradeoffs Y" is the one that requires evidence. The null hypothesis is that it doesn't. What's the argument here? Is it OK then to question the existence of the Apollo program because “the yanks never went to the moon” is the null hypothesis? We've plenty of evidence that Rust offers better guarantees than C (even though with your reasoning there could be a hidden second-order effect that makes Rust actually worse than C, we cannot be sure after all, the Rust compiler is slower than C's… /s). Now since Zig doesn't address the most prominent source of critical defects in C, the null hypothesis is that it won't be an improvement compared to C. (I actually don't think that hypothesis is true either, C is very dated and there are tons of room for small UX improvements, but getting an improvement as big as what Rust offers is a big step to climb with small improvements). > As I said, software correctness is my thing. When I saw Zig's brilliant, revolutionary design, I thought Yet you're like two thousand words in and you've not even begun to hint at what part of Zig designs makes it especially good for correctness compared to C. > However, anyone who says we already know is not telling the truth, and probably has a shaky understanding of the subject. Like with climate modeling or immunology, we're far from knowing as much as we'd like, but that doesn't mean we know nothing: for instance we know that 1) distributed systems are practically impossible to get right without tools (and TLA+ is a blessing), and we know that 2) manual memory management isn't tractable by a human without assistance. For these two problems, we have decades of empirical evidence that shows that the human brain just isn't able to do it reliably. We also know that 3) so far sanitizer and other runtime tools haven't been enough to get it right in practice. Zig basically says that even if 2) is true, 3) will not hold for long because it will have “better tools”® than what exists for C. Hard to tell how far these tools will eventually go, but for the moment it has yet to prove anything on that front. > You're saying it's not good because it doesn't try to completely eliminate such errors? Yes I am, because ”eliminating completely* such errors” is the standard for every language designed after 1985 that has reached even limited use. (And we're not talking about some low-level stuff that only C or C++ could do, but about a product that competes with another written mostly in JavaScript). By letting this kind of errors happen, it's a step back of more than 35 years ! And by “happen” or “completely eliminate” I mean “happen enough that it surfaces significantly to the user” (and resp.), I'm not arguing that it should be proven that it cannot happen (in fact, even Rust does make such a claim),but at least it should be exceptional in practice, not one of your most common issue keyword on github… If Zig empirically had like 0.1% memory issues, then arguing that improving on any other fronts is more important would be fine (like Go not being memory safe in the presence of data race, we can agree that this isn't a significant factor in software reliability using that language and move on), but it's not what's happening. What happens is that the only commercial use of Zig so far is facing a double-digit amount of memory-related crash reported by its users. We're not talking about CVEs found by an adversary here, just Joe the user who has his software randomly crashing at startup. Correctness you said? > Zig's memory safety story is not perfect because the cost of perfection, Zig's philosophy believes, is too high, to the point of working against the goal of correctness. As a side note, this is a strawman, Rust doesn't aim at ”perfection” either as it's happily relying on unsafe code when needed, and Rust pragmatic solution to improving memory safety in unsafe code was Miri, a runtime sanitizer, not some kind of proof assistant or anything). There's also a runtime check for overflows or out of bounds access, not dependent types to aim at soundness perfection.

by pron 4y ago

littlestymaar 4y ago

> No. The claim "design with tradeoffs X leads to more correct programs than design with tradeoffs Y" is the one that requires evidence. The null hypothesis is that it doesn't. What's the argument here? Is it OK then to question the existence of the Apollo program because “the yanks never went to the moon” is the null hypothesis? We've plenty of evidence that Rust offers better guarantees than C (even though with your reasoning there could be a hidden second-order effect that makes Rust actually worse than C, we cannot be sure after all, the Rust compiler is slower than C's… /s). Now since Zig doesn't address the most prominent source of critical defects in C, the null hypothesis is that it won't be an improvement compared to C. (I actually don't think that hypothesis is true either, C is very dated and there are tons of room for small UX improvements, but getting an improvement as big as what Rust offers is a big step to climb with small improvements). > As I said, software correctness is my thing. When I saw Zig's brilliant, revolutionary design, I thought Yet you're like two thousand words in and you've not even begun to hint at what part of Zig designs makes it especially good for correctness compared to C. > However, anyone who says we already know is not telling the truth, and probably has a shaky understanding of the subject. Like with climate modeling or immunology, we're far from knowing as much as we'd like, but that doesn't mean we know nothing: for instance we know that 1) distributed systems are practically impossible to get right without tools (and TLA+ is a blessing), and we know that 2) manual memory management isn't tractable by a human without assistance. For these two problems, we have decades of empirical evidence that shows that the human brain just isn't able to do it reliably. We also know that 3) so far sanitizer and other runtime tools haven't been enough to get it right in practice. Zig basically says that even if 2) is true, 3) will not hold for long because it will have “better tools”® than what exists for C. Hard to tell how far these tools will eventually go, but for the moment it has yet to prove anything on that front. > You're saying it's not good because it doesn't try to completely eliminate such errors? Yes I am, because ”eliminating completely* such errors” is the standard for every language designed after 1985 that has reached even limited use. (And we're not talking about some low-level stuff that only C or C++ could do, but about a product that competes with another written mostly in JavaScript). By letting this kind of errors happen, it's a step back of more than 35 years ! And by “happen” or “completely eliminate” I mean “happen enough that it surfaces significantly to the user” (and resp.), I'm not arguing that it should be proven that it cannot happen (in fact, even Rust does make such a claim),but at least it should be exceptional in practice, not one of your most common issue keyword on github… If Zig empirically had like 0.1% memory issues, then arguing that improving on any other fronts is more important would be fine (like Go not being memory safe in the presence of data race, we can agree that this isn't a significant factor in software reliability using that language and move on), but it's not what's happening. What happens is that the only commercial use of Zig so far is facing a double-digit amount of memory-related crash reported by its users. We're not talking about CVEs found by an adversary here, just Joe the user who has his software randomly crashing at startup. Correctness you said? > Zig's memory safety story is not perfect because the cost of perfection, Zig's philosophy believes, is too high, to the point of working against the goal of correctness. As a side note, this is a strawman, Rust doesn't aim at ”perfection” either as it's happily relying on unsafe code when needed, and Rust pragmatic solution to improving memory safety in unsafe code was Miri, a runtime sanitizer, not some kind of proof assistant or anything). There's also a runtime check for overflows or out of bounds access, not dependent types to aim at soundness perfection.