Advent of Code 2018, in Coq

Re:Advent of Code 2018, in Coq by seanmcdirmid on Monday February 18, 2019 @09:21PM (#19196189)

> I suppose one could say Coq is good enough, with bugs.

Wait, isn't Coq verified by itself?

[ Parent | on HN ]

Re:Advent of Code 2018, in Coq by syrak on Monday February 18, 2019 @09:37PM (#19196224)

The Coq compiler is unverified, it is written in OCaml.

It's not possible for Coq's consistency to be verified in itself, thanks to Gödel's second incompleteness theorem. However there are still various other aspects of the compiler that could be verified in principle. The CertiCoq project is actively going in that direction.

[ Parent | on HN ]

Re:Advent of Code 2018, in Coq by quickthrower2 on Tuesday February 19, 2019 @03:25PM (#19202440)

I love this comment, because there is this pie in the sky mathematical idea, with direct consequences for practical coding.

[ Parent | on HN ]