> But that's wrong. Everything has a cost. And formalisms like Rust are still pityful attempts at constructing "formally correct" software. There might be some software that is "completely" verified, but at a cost that is simply not justifiable for the vast number of applications. Ignoring the fact that most real-world problems are ill-specified from the start.
You seem to be saying "it's hard to verify everything, so we shouldn't even attempt to verify anything," which is silly. I've found having memory safety to be a huge win, even if the Rust compiler can't verify that my program is doing the right thing.
You seem to be saying "it's hard to verify everything, so we shouldn't even attempt to verify anything," which is silly. I've found having memory safety to be a huge win, even if the Rust compiler can't verify that my program is doing the right thing.