Hacker News Reader

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

View on HN

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

> types are propositions

ML and Coq types, yes. Java, C types? Not so much.

Call them "illogical propositions".

Reply on news.ycombinator.com