News for hackers. Stuff that matters.

A comment on Advent of Code 2018, in Coq. Parent comment

Re:Advent of Code 2018, in Coq by dmitriid on Tuesday February 19, 2019 @03:53AM (#19197572)
> 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 :) ).

[ Parent | on HN ]
Re:Advent of Code 2018, in Coq by bjz_ on Tuesday February 19, 2019 @04:28AM (#19197735)
> 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.

[ Parent | on HN ]
Re:Advent of Code 2018, in Coq by frabert on Tuesday February 19, 2019 @04:57AM (#19197868)
> types are propositions

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

[ Parent | on HN ]
Re:Advent of Code 2018, in Coq by bunderbunder on Tuesday February 19, 2019 @10:07AM (#19199404)
Call them "illogical propositions".
[ Parent | on HN ]