4 ms·
Every time someone points out this tutorial and I see again the even_0 and even_S constructors of the even predicate, I am reminded of the quote where FORTRAN i
by pascal_cuoq 16y ago
Every time someone points out this tutorial and I see again the even_0 and even_S constructors of the even predicate, I am reminded of the quote where FORTRAN is called a high-level language because, unlike assembly, it doesn't force the programmer to make up names for intermediate expressions.
There are good reasons why even_0 and even_S need to have names, but I sure hope that we will one day look back on Coq as the assembly of computer-assisted proofs.
- scscsc 16y agoI somewhat agree. I have a stronger postulate: current proof assistants are worse for writing proofs than machine language. There is a reason not to panic: it can only get better, not worse...
- jbapple 16y agopascal_cuoq said: "There are good reasons why even_0 and even_S need to have names, but I sure hope that we will one day look back on Coq as the assembly of computer-assisted proofs." For predicates that can be computed in coq, we can do away with the names: Fixpoint even n := match n with | 0 => True | 1 => False | S (S m) => even m end. Note that "True" and "False" are propositions (have sort "Prop") with trivial and no proofs, respectively, and are not "true" and "false", which are the constructors of the inductive type "bool". If the return type were changed to bool, "even n = true" (rather than just "even n") would be a predicate meaning "n is an even natural number". Additionally, your wish is already coming true! For certain types of problems, coq can be hooked up to external solvers (for SAT, for instance) which generate proof terms that are then checked by coq. See http://www.lri.fr/~melquion/doc/09-calculemus-article.pdf http://www.lri.fr/~melquion/doc/09-calculemus-article.pdf for an example.