Comment by Ygg2

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