Comment by Ygg2
14 hours ago
> 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 see with a technology whose excited but few fans 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.