Those other "highly effective program manipulations" include refactoring and modifications which involve changing parameter and return types. While I understand

Those other "highly effective program manipulations" include refactoring and modifications which involve changing parameter and return types. While I understand what you're saying, to myself it's pretty clear that there's a wide gap between these two scenarios: * Changing the collection's type and not knowing until runtime -- when your program crashes -- that it's being used wrong. * Changing the collection's type and the program refusing to compile until all usage is corrected. Because of this, I don't agree with the most modifier you're attempting to apply. The difference to me is confidence. In the former, how confident am I that I didn't miss a use-case on some branch? Considering that the program will crash or otherwise fail to operate, that seems like something I want to be pretty confident about. It's very useful to have something telling you that everything looks OK. That something can be testing, but why rely on writing good tests when we have formal proof systems available?