4 ms·
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 conven
by gabrielmoshe 8y ago
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/ https://coq.inria.fr/
- davidgrenier 8y agoAt 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/ https://softwarefoundations.cis.upenn.edu/