3 ms·
> What's the argument here? The argument is that you don't have a hypothesis and then put the burden of proofs on others to prove that it's untrue. The justifi
by pron 4y ago
> What's the argument here?
The argument is that you don't have a hypothesis and then put the burden of proofs on others to prove that it's untrue. The justification for why science must work like this is that most associations must not be true correlations.
> We've plenty of evidence that Rust offers better guarantees than C
True, but our starting point was that neither C (let's call it 0 sound safety) nor Idris (let's call it 100 sound safety) are the best approach, i.e. we know that the most effective way is something in the middle, i.e. we already know that more soundness is sometimes better and sometimes worse.
> Now since Zig doesn't address the most prominent source of critical defects in C
No, that's your claim. Zig is as different from C as Rust is. Zig does make sound guarantees of spatial memory safety (which neither C nor C++ do), and unlike C or C++, pointers cannot be created from "thin air" with pointer arithmetic or with hidden casts such as unions, i.e. Zig has precise knowledge of what a pointer is. This makes tooling for detecting temporal memory unsafely much more powerful and precise in Zig than in either C or C++.
> 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.
I hope I now did. Plus, its expressiveness is that of C++ (or Rust), not C, while being very simple (two languages are as expressive if there aren't programs in one that require more lines in the other than by a constant factor; C++ has program facilities that require exponentially more lines in C).
> but that doesn't mean we know nothing
Well, whether Rust makes it easier to write correct programs is something we don't know.
> so far sanitizer and other runtime tools haven't been enough to get it right in practice.
You're talking about sanitisers for C/C++. Zig is very different. Again -- full spatial safety, and precise pointers.
> but for the moment it has yet to prove anything on that front.
Sure, and Rust too.
> Yes I am, because ”eliminating completely* such errors” is the standard for every language designed after 1985 that has reached even limited use
That is a very bad argument. You could just as well say that the standard is not to have safety based on substructural types because that's probably too costly. I think it's funny to pretend that Rust's way to memory safety isn't very different from, say, Java's, and doesn't come at a significant cost. It obviously is, and does, and the question we don't know the answer to is: is that a better tradeoff than Zig's?
Also, the number of low-level languages designed after 1985 that have reached even limited use is too small to make any generalisation, let alone a standard, and it opens you to a far worse argument: despite the popularity of memory safety in the application space, no low-level language that has achieved significant use has been memory-safe. Don't try to build statistics on a small sample. Not only is the argument bad, but it can just as easily be turned against you.
> And by “happen” or “completely eliminate” I mean “happen enough that it surfaces significantly to the user”
This is the argument Rust is making that those who aren't so involved in software correctness find compelling, but it is nonetheless false. It goes like this: we have lots of kinds of bugs, if we can eliminate some with soundness, then that must be better! Most formal methods researchers found that argument so convincing in the 70s that they almost accepted it axiomatically. Except it turned out not to be true. Less sound approaches proved more effective overall despite not "eliminating" classes of bugs. But we don't know where the sweet spot is yet.
> Correctness you said?
I don't understand your complaint. First, I hope you're not claiming that programs written in Rust don't have very serious bugs, just as bad as segfaults. Second, you're trying to draw a trend out of tiny samples again; this never ends well. You're a step away from saying, 100% of commercial Zig programs crash, <100% commercial C programs crash, therefore it's better not to have spatial memory safety. It's like talking about a person who dies from some illness, and saying, see, that's Western medicine for you.
Anyway, my personal opinion of Rust, as someone who mostly programs in C++ is that it doesn't address the two main issues with the language -- a complex language that requires non-local reasoning, making reviews hard and slow and requiring too much thought about the language rather than the algorithm, and a slow build-test cycle that results in less testing than more "agile" languages. Zig, on the other hand, starts with those two problems, so while I have no idea whether Zig (or Rust for that matter) would ever succeed in the market and that I would ever get to use it "in production", the language that would address my biggest issues in low-level programming would look much more like Zig than like Rust.
Moreover, I think Rust made the same big mistake C++ did: trying to get a low-level language to look like a high-level one on the page (so-called "zero-cost abstractions"). I think that design philosophy has little pros and too many cons.
- pron 4y agoP.S. In the nineties I worked on a big defence project that was written half in C++ and half in Ada. Ada was the Rust of the day, plus it had the weight of the US DoD behind it, which was no small thing. But at the time it was a much more complex language than C++, so we had to have "language lawyers", and, just as bad, its build time was much worse, that in the end we just couldn't test it as well as our more ostensibly sloppy C++ code, the result being that we gradually shifted away from Ada. I'm not saying that the vision of the seventies of "more language; more formal soundness" is always wrong, but it's certainly isn't always right. The biggest improvement in software correctness that saved us from the total software collapse prophesied by the "formalists" of the seventies, like Dijkstra and Tony Hoare, was the advent of automated unit tests. It's been so effective that it surprised those formalists (like Hoare) as well as confounded those PL people who believed that more and better types are always better (so much so that correctness differences between languages have been very hard to find in recent years except in special circumstances, such as JS vs TypeScript). We learnt that "more language" isn't always the best answer, although sometimes it could be. We just don't know where the "best" tradeoffs are, or even if they're universal. In the past couple of decades we've also learnt more about software correctness from complexity theory, "hard" results that just weren't known to Dijkstra, and that put limits on the effectiveness of soundness. We also learnt some empirical "soft" results -- such as this one [1] -- that showed that sometimes soundness just pushes the bugs elsewhere (i.e. people write code that satisfies the language, yet manage to do this without addressing the fundamental issue, so the catastrophic bug just manifests differently). None of that is surprising in retrospect. Bugs occur due to a lack of exhaustiveness in human reasoning (or even machine reasoning, as we now have the complexity theory to understand that), so if you're writing an algorithm whose object-lifetimes considerations are too onerous for humans, it is likely that there are other aspects of it that are equally onerous. So what is the right price to pay to prevent that algorithm failing due to use-after-free specifically? So when a language offers to eliminate certain classes of bugs, even important classes, but possibly at the cost to both static and dynamic functional reasoning -- through reviews and tests -- it is in no position to say that it's obviously the right approach, and that's why there's no consensus that it is. Zig opts to eliminate fewer classes of bugs, up to the point that doing so is free. That's certainly an equally valid hypothesis, a-priori at least, and it will be interesting to see how things develop. [1]: https://www.usenix.org/system/files/conference/osdi14/osdi14-paper-yuan.pdf https://www.usenix.org/system/files/conference/osdi14/osdi14...