> What I would be terrified of in Coq is some tiny change in business requirements ends up pulling the linchpin out of some fundamental premise way down at the bottom of your stack of proofs, this forcing you to go and fix everything. Sort of the mother of all brittle testing scenarios.
Isn't the same true for static typing? One small business requirement changes, you change a foundational type, and suddenly all your code needs to adapt.
Of course this is true with dynamic typing too, but at least you don't know.
> Isn't the same true for static typing? One small business requirement changes, you change a foundational type
Business changes are usually changes in logic, not in types. So it's mostly "our cashback is now calculated in percentage of the sum, not as a fixed sum" etc. Of course, this may still have repercussions through the entire system. I don't know how it would work in Coq (I don't know Coq :) ).
> Business changes are usually changes in logic, not in types.
Types _are_ logical propositions. In languages like Coq they are more expressive, and it's easier to leverage them as a way to constrain your implementation. Of course it's just a model, and there can be bugs in the specification, so it's not a silver bullet.
I guess. My experience has been that it's more a case with, for lack of a better term, "old school" OOP.
SOLID helps a lot with that sort of thing. Avoiding inheritance like the plague helps a lot. I slightly hate that I said old school, because Smalltalk-style tell-don't-ask helps a lot.
I think that the idiomatic ways of structuring code in the ML family of languages help the most, because they tend to be pretty radical about limiting scope of visibility. But they also tend to make more of a muddle of things than they're worth in algol-style languages.
Isn't the same true for static typing? One small business requirement changes, you change a foundational type, and suddenly all your code needs to adapt.
Of course this is true with dynamic typing too, but at least you don't know.