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