> This is a false equivalence, as not all bugs are the same and so cannot be trivially equated in this fashion.
Correct, and I tried hard not to make that equivalence.
> Memory safety violations permit classes of bugs of significantly higher severity than other types of bugs.
This is not known to be true after eliminating 95% of memory safety violations.
> Your off-hand disclaimer of "the same or different ones of equal severity" doesn't mean anything, because you cannot predict the severity or scope of even trivial memory unsoundness, so your heuristic arguments of preferring lower cost methods simply don't work.
Ah! Now that is 100% true, but it cuts both ways. Of course it's a problem that we can't know in advance what would be a severe bug or it's probability, but saying let's shift resources into sound methods in areas where they happen to work implicitly makes such guess. It's alright to acknowledge that measuring the effectiveness is hard, but that also means we can't presuppose the effectiveness of something just because it has an easy to understand mathematical property. I'm not arguing for or against sound methods; I'm saying that since the question is empirical, it must be answered by empirical means as that is the only way to answer it.
A pragmatic argument may be that you'd rather risk overspending on correctness than underspending, which essentially means: spend whatever you can on soundness whenever you can have it. The problem is that the world just doesn't work this way, because budgets are limited, and any work that is done to increase confidence in one property must, necessarily, come at the expense of other work that may also have value. There is simply no escape from measuring the cost/benefit of an economic activity that has a non-zero cost.
If I fly on a plane I want to know that the company doing the avionics spent its assurance budget in the way that eliminated most bugs, not that it spent it on ensuring memory safety (when I was working on avionics, we didn't use deductive methods even though they were available at the time precisely because their ROI was low and that's bad for correctness where you want every dollar to do the most good).
> Memory safety is NOT an underwhelming property. Arguably, all other properties of your program derive from memory safety.
Except this is the starting point for most software. If your goal is to get to where most software is already is -- I would very much characterise it as underwhelming.
> If you have to use an unsafe language that permits violating memory safety, say for performance reasons, and you have any kind of attack surface, then ensuring memory safety is important. Probably more important than most other properties you otherwise think are important due to #1.
Yes, but how much should you invest in getting from 0 safety to 90% vs how much from 90% to 100%?
> Arguments that you eliminated 80% of trivial memory unsoundness is simply not compelling if it leaves all of the subtle, more dangerous ones in place.
I agree, but again -- it cuts both ways. If you invest a significant amount of effort in eliminating the last 5% of memory safety violations you cannot claim that it's more effective than spending your effort elsewhere. All I'm saying is that these are empirical questions and the fact that whether something is sound or not has a clear yes/no answer doesn't really help tackle the empirical problem.
> The long history of security vulnerabilities is a main driver in the interest in soundness among researchers, contra your claims that that this obsession has no association with real-world needs.
This is clearly not true, because the focus on soundness has only decreased over the past 50 years and continues to decrease. In the 70s it was soundness is the only way. Now there's more research into unsound methods.