3 ms·
Why don't they make it less "hard" by allowing the use of a good proof-oriented programming language, with importable packages of established proofs and techniq
by OutOfHere 1y ago
Why don't they make it less "hard" by allowing the use of a good proof-oriented programming language, with importable packages of established proofs and techniques, instead of having to rewrite each proof from scratch?
- Jtsummers 1y ago> Why don't they make it less "hard" by allowing the use of a good proof-oriented programming language [emphasis added] Who's preventing this now? Take a look at things like Software Foundations and other works which are built on automated or interactive proof systems. https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/