Yes, some important programs can be soundly verified and various local properties can make that …

I think it's reasonable to look forward to verifying that small Rust libraries use 'unsafe' correctly. That alone would be really helpful.

P.S. A focus on soundness does not, I believe, help the cause of more correct software but distracts from techniques that have proven more fruitful in practice (and supported by theory) -- sometimes to the surprise of those who used to think that soundness is the only way, e.g. http://users.csc.calpoly.edu/~gfisher/classes/509/handouts/h... . This happens over and over: there is some important improvement in sound methods while at the same time unsound methods are making much bigger strides toward more correct software in practice. Here's just one very recent example (which isn't even necessarily state-of-the-art in unsound methods): https://antithesis.com Of course, this is a very complex topic, because there are some specific situations where sound techniques are more powerful and practical.

Hi Mr Presler, I don't know if you realize that you've preached the exact same argument here on HN a hundred time for the past 6 years at least, without ever adding nuance after the many comments you've received on the topic here. You're not entirely wrong, but also far from entirely correct as half the world interested in the topic has had many chances to show you over the hundreds of time you've made that argument here. And what's fascinating (besides your relentless preaching) is that the complete absence of any evolution in your position after all this time show that you haven't learned anything from these discussions with others, nothing. That really sounds like pathological close-mindedness at that point. It means that everybody is losing there time when engaging with you, and that's really something you should try and think about. Regards