3 ms·
>Firstly, I never said sound methods ought to be used. You kind of did say this: "soundness for some critical properties is absolutely warranted". It seemed cl
by foldr 2y ago
>Firstly, I never said sound methods ought to be used.
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".
>if you cannot rely on it then your system effectively has no guarantees of any kind.
In the real world you cannot rely on anything absolutely. All guarantees are probabilistic. Rust, for example, does not have a formally verified compiler, so you cannot be absolutely sure that your provably memory safe code will actually compile down to memory safe machine code (or indeed to machine code that does what it's supposed to do in any other respect). Does that mean we need to go off and formally verify the Rust compiler because otherwise none of our systems will have guarantees of any kind? If it doesn't, then note that you are making exactly the same kind of cost/benefit analysis that pron is talking about.
It's easy to list lots of things that systems 'should' do. In a realistic scenario there is a budget of time/effort/attention/money.
- naasking 2y ago> 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.
- foldr 2y agoI think "sound methods" in this context just means methods that guarantee soundness. You can have soundness without sound methods, but you can't know (for sure) that you have it.