3 ms·

P.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

by pron 4y ago

P.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...

littlestymaar 4y ago
You're basically saying the same thing over and over between different posts, but here's one interesting thing: > 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. The thing is that you have lifetimes considerations in Zig too. You need to know when to free memory, so you explicitly need to reason about it, just like in Rust in the worse case (when RAII alone isn't enough) but you don't have tools to helps you know when to free and when not to (and only tools to diagnose when you've missed it) so Zig actually adds cognitive burden, not removes it. In the end you'll be reclaiming the memory at the same place (which is where the object is not used anymore and safe to free). And you keep pointing to reviews and tests, as if rust made it harder, when in fact it makes it marginally easier than for most languages, with its built-in test framework well integrated in the entire stack, and the ability to see where mutations happen. Of course it's not revolutionary nor even unique, but on those two specific subjects in is in fact in among the best languages out there. So you keep talking about Rust's cost, but the thing is that you can't really pinpoint what types of cost this is about (except with the hand-wavy concept of “language complexity”), and the examples you give are off.
- pron 4y ago
  > You need to know when to free memory, so you explicitly need to reason about it, just like in Rust Obviously! But my point was that that reasoning isn't additive. If an algorithm is complex enough that you have to carefully reason about its object lifetime, then you might have to carefully reason about it even if you're guaranteed to get the lifetime right. Or, rather, sometimes you might, sometimes maybe not, and other times the extra burden of the language is just a chore. > so Zig actually adds cognitive burden, not removes it In that regard -- absolutely, in others, it reduces it. Rust's soundness obviously does some good things -- at a price. The question isn't whether those things work, but if they're worth the price. I'm not saying Rust doesn't give me value for my effort; we just don't know if it's more or less than what Zig gives us. > but on those two specific subjects in is in fact in among the best languages out there. Except Zig takes that to another level. Rust has some brilliant innovations -- like the borrow checker -- but Zig's entire design is a quite revolutionary, and in multiple ways. That's why I find comparisons between it and C to be so misleading. We've never seen anything like it before. > So you keep talking about Rust's cost, but the thing is that you can't really pinpoint what types of cost this is about I don't need to justify why Rust isn't the best approach out there; the onus is on Rust. If we knew which of Rust's approach or Zig's or maybe others altogether worked best, then we wouldn't be trying all of them. We are because we don't know. But assumptions that soundness was the best approach proved wrong in a surprising ways in the past, and a combination of soundness and unsoundness (those "hand wavy" techniques of testing and reviews) are what proved effective. Bot Zig and Rust believe in such a combination, only in different measures. Perhaps in time we'll find out which works better, but you can't say, "fine, sometimes soundness is better and sometimes it's worse, but my mix is better than yours because it has more soundness." Now, I'm not trying to convince you, or anyone, that Zig's approach to correctness works better than Rust's; we simply don't know. What I'm trying to get across is why both approaches are novel and interesting enough that we need to try both. BTW, there's another axis we need to consider. The goal of software correctness from the industry's perspective is not how to write more correct software, but how to write more correct software with the programmers we have. That's why, even though it's possible that the few who can make effective use of Idris might (although maybe not) be able to produce more correct programs than others, few consider Idris as the probably solution to the problem because so few programmers would be able to put it to good use. A language that improves correctness by X around for Y programmers contributes less overall to correctness than a language that improves it by X/2 for 5Y programmers.

by pron 4y ago

littlestymaar 4y ago

You're basically saying the same thing over and over between different posts, but here's one interesting thing: > 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. The thing is that you have lifetimes considerations in Zig too. You need to know when to free memory, so you explicitly need to reason about it, just like in Rust in the worse case (when RAII alone isn't enough) but you don't have tools to helps you know when to free and when not to (and only tools to diagnose when you've missed it) so Zig actually adds cognitive burden, not removes it. In the end you'll be reclaiming the memory at the same place (which is where the object is not used anymore and safe to free). And you keep pointing to reviews and tests, as if rust made it harder, when in fact it makes it marginally easier than for most languages, with its built-in test framework well integrated in the entire stack, and the ability to see where mutations happen. Of course it's not revolutionary nor even unique, but on those two specific subjects in is in fact in among the best languages out there. So you keep talking about Rust's cost, but the thing is that you can't really pinpoint what types of cost this is about (except with the hand-wavy concept of “language complexity”), and the examples you give are off.

pron 4y ago
> You need to know when to free memory, so you explicitly need to reason about it, just like in Rust Obviously! But my point was that that reasoning isn't additive. If an algorithm is complex enough that you have to carefully reason about its object lifetime, then you might have to carefully reason about it even if you're guaranteed to get the lifetime right. Or, rather, sometimes you might, sometimes maybe not, and other times the extra burden of the language is just a chore. > so Zig actually adds cognitive burden, not removes it In that regard -- absolutely, in others, it reduces it. Rust's soundness obviously does some good things -- at a price. The question isn't whether those things work, but if they're worth the price. I'm not saying Rust doesn't give me value for my effort; we just don't know if it's more or less than what Zig gives us. > but on those two specific subjects in is in fact in among the best languages out there. Except Zig takes that to another level. Rust has some brilliant innovations -- like the borrow checker -- but Zig's entire design is a quite revolutionary, and in multiple ways. That's why I find comparisons between it and C to be so misleading. We've never seen anything like it before. > So you keep talking about Rust's cost, but the thing is that you can't really pinpoint what types of cost this is about I don't need to justify why Rust isn't the best approach out there; the onus is on Rust. If we knew which of Rust's approach or Zig's or maybe others altogether worked best, then we wouldn't be trying all of them. We are because we don't know. But assumptions that soundness was the best approach proved wrong in a surprising ways in the past, and a combination of soundness and unsoundness (those "hand wavy" techniques of testing and reviews) are what proved effective. Bot Zig and Rust believe in such a combination, only in different measures. Perhaps in time we'll find out which works better, but you can't say, "fine, sometimes soundness is better and sometimes it's worse, but my mix is better than yours because it has more soundness." Now, I'm not trying to convince you, or anyone, that Zig's approach to correctness works better than Rust's; we simply don't know. What I'm trying to get across is why both approaches are novel and interesting enough that we need to try both. BTW, there's another axis we need to consider. The goal of software correctness from the industry's perspective is not how to write more correct software, but how to write more correct software with the programmers we have. That's why, even though it's possible that the few who can make effective use of Idris might (although maybe not) be able to produce more correct programs than others, few consider Idris as the probably solution to the problem because so few programmers would be able to put it to good use. A language that improves correctness by X around for Y programmers contributes less overall to correctness than a language that improves it by X/2 for 5Y programmers.