Comment by pron
1 day ago
> A program that can't express H (72 in decimal) in Hello world is about as divorced from practicals as you can get
Huh? I was giving an example of how we make undecidable properties trivial in languages. It can be any property. It's easy to see that Rust does the same with memory safety, i.e. through an inductive invariant, because every statement in Rust maintains the invariant.
> Yes, but it relies very little on human verification.
Of course. It shouldn't rely on human verification at all. That's how we design type systems. But because an inductive invariant is inherently conservative and must reject correct programs, there is additional human effort required -- not to verify the property, but to stay within the confines of the inductive invariant. In Rust terms, the compiler takes care of memory safety, but you need to put an effort into expressing memory-safe programs in Rust to fit within Rust's constraints, which are, necessarily more restrictive than memory safety (because they must use an inductive invariant).
> And I'm saying it as a programmer field we should monotonically approach the ideal by removing languages that don't support it.
And I'm saying that what we've learnt over the past five decades is that more soundness does not necessarily mean getting closer to the ideal. Sometimes more soundness gets us further away from the ideal.
> Also seatbelts are sometimes worse, doesn't mean we shoud abolish them for seatbelts-less Pintos.
No one is suggesting that, it's just that what you're referring to as seatbelts could sometimes do more harm than good even for safety. We have empirical evidence that real seatbelts increase safety; things are nowhere near as clear for language soundness.
Sure, C is so exceptionally weak that we can do better than that, and there's no doubt Rust is better on correctness than C, but that's not the same as saying Rust is better on correctness than any language that makes fewer guarantees than Rust. Why? Because, again, we've seen that the benefits of soundness are not linear -- they help until they start hurting. Knowing where that point is is not easy.
> Huh? I was giving an example of how we make undecidable properties trivial in languages. It can be any property.
Yes, but insisting you have to be 100% machine verified, while the program is correct, it is impractical. While it might be Turing complete, it can't express equivalent behavior to a C program.
This is one of those quotes like "Don't let perfect be the enemy of good".
Look at your definition of memory safety, by it nothing other than ATS or some Lisp derivative running on a Lisp machine is actually memory safe.
Sure, it's theoretically sound, but it's not pragmatical.
> We have empirical evidence that real seatbelts increase safety; things are nowhere near as clear for language soundness.
We have empirical evidence that Rust has measurable impact on bugs, especially memory safety ones.
> While it might be Turing complete, it can't express equivalent behavior to a C program.
Neither can safe Rust! But this is easier to see in my example because parity is a very functional, as opposed to technical property.
> This is one of those quotes like "Don't let perfect be the enemy of good".
I am not calling for perfect. Quite the opposite. I am saying that software correctness is extremely complicated, and even the biggest researchers in the field have been surprised by outcomes that were counterintuitive to them. Yet you seem to have decided that Rust gives the best results of everything that's available, while I have my doubts, especially because I see how people are turning away from Rust and how much it struggles to capture a significant portion of the low-level programming market even at its quite advanced age. I don't think there's a single language in the top ten that's had such low adoption at Rust's current age, and that's not the kind of thing you expect to see with a technology whose excited but small fanbase claim to hit an excellent pragmatic sweet spot.
> We have empirical evidence that Rust has measurable impact on bugs, especially memory safety ones.
Compared to C, yes. That's exactly what you expect if more sound guarantees help and then hurt -- a language with some sound guarantees to be better than a language with virtually none. But that is not to say that other languages with either more or less sound guarantees aren't an even better sweet spot.