News for hackers. Stuff that matters.

A comment on How Math’s Most Famous Proof Nearly Broke (2015). Parent comment

Re:How Math’s Most Famous Proof Nearly Broke (2015) by gabrielmoshe on Friday December 21, 2018 @07:22AM (#18732899)
Yes! There are several different languages and systems used for coding proofs. Coq [1] is probably the most well known. But, as you alluded to, it is not convenient (or easy) to code all proofs in such a style.

1. https://coq.inria.fr/

[ Parent | on HN ]
Re:How Math’s Most Famous Proof Nearly Broke (2015) by davidgrenier on Friday December 21, 2018 @08:17AM (#18733077)
At OPLSS 14, Andrew Appel characterized programming in Coq as the world's best video game, I would have to say it's a close second.

I recall it was accessible if you had programmed in an ML, start here: https://softwarefoundations.cis.upenn.edu/

[ Parent | on HN ]