> how expensive and non-compositional soundness necessarily is
It is "deeper" properties (these are defined more robustly as those requiring a greater number of alternating universal and existential quantifiers) that are usually non-compositional and expensive to prove (and soundness means proof). Simple properties are easy to prove and can be made compositional, but they're also less valuable.
> So why wouldn't you?
No reason, except for the fact that you've defended against things that are easy to defend against easily and didn't defend against the hard things. In other words, of course you should prove as many properties as you can for a low cost, but don't exaggerate what it is that you've gained by doing so. That is precisely the delta between "can" and "need" that I was referring to. It's cool that I can get some extra security cheaply, but if that extra security amounts to 5%, then its value is not that high.
> There is no cost-benefit here, it's just benefit.
Of course there is. When the benefit is low then it's particularly easy to offset by other concerns, e.g. the speed at which I can churn out code or the cost of writing a compiler for an exotic architecture, a relatively common concern in the embedded space.
In any event, I always prefer typed languages when building big/important software (I've rarely used untyped languages), but remember that the original post is not about the simple properties that we get cheaply in typed languages, but how non-aliasing can make proving deeper properties easier. And what I was saying is that these proofs are nowhere near cost effective in most cases even after they've made a little easier.
It is "deeper" properties (these are defined more robustly as those requiring a greater number of alternating universal and existential quantifiers) that are usually non-compositional and expensive to prove (and soundness means proof). Simple properties are easy to prove and can be made compositional, but they're also less valuable.
> So why wouldn't you?
No reason, except for the fact that you've defended against things that are easy to defend against easily and didn't defend against the hard things. In other words, of course you should prove as many properties as you can for a low cost, but don't exaggerate what it is that you've gained by doing so. That is precisely the delta between "can" and "need" that I was referring to. It's cool that I can get some extra security cheaply, but if that extra security amounts to 5%, then its value is not that high.
> There is no cost-benefit here, it's just benefit.
Of course there is. When the benefit is low then it's particularly easy to offset by other concerns, e.g. the speed at which I can churn out code or the cost of writing a compiler for an exotic architecture, a relatively common concern in the embedded space.
In any event, I always prefer typed languages when building big/important software (I've rarely used untyped languages), but remember that the original post is not about the simple properties that we get cheaply in typed languages, but how non-aliasing can make proving deeper properties easier. And what I was saying is that these proofs are nowhere near cost effective in most cases even after they've made a little easier.