> 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 easie

> 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.