> You kind of did say this: "soundness for some critical properties is absolutely warranted". It seemed clear that you were taking memory safety to be one of th

> You kind of did say this: "soundness for some critical properties is absolutely warranted". It seemed clear that you were taking memory safety to be one of the "critical properties". You can achieve soundness without "sound methods" in the formal sense that you were using the term. > If it doesn't, then note that you are making exactly the same kind of cost/benefit analysis that pron is talking about. I disagree, there's at least an order of magnitude difference between what we're discussing (probably more). pron is tossing around numbers like eliminating 95% of memory safety bugs, where the safety of runtime checked arrays will eliminate more like 99.99% of memory safety bugs, where that 0.01% allows for the chance the you made a mistake in your checked array implementation. There is simply no equating the two.