maxklein said: "I'd never specialise in this language because everyone will turn to a teenager when you are listing your skills."
Coq is not a general-purpose programming language. People who "specialize in this language" generally work in a field where everyone is familiar with the name "coq" and nobody bats an eye.
Are you sure about that? I've seen co-workers suggest the use of Coq, only to see a room full of managers and peers burst out in laughter. Coq won't catch on in many places where it'd be very useful solely because of its name.
Even worse, you'll link them to sites with good arguments for exactly where it is useful... named "10 places where coq comes in handy" and "You and coq: a good fit" or "Do it faster with coq"
KERMIT said: "Are you sure about that? I've seen co-workers suggest the use of Coq, only to see a room full of managers and peers burst out in laughter."
I think my claim that "People who 'specialize in this language' generally work in a field where everyone is familiar with the name 'coq' and nobody bats an eye." is sufficiently specific that it is not in contradiction with your anecdote. I used the word "specialize" because I was responding to a claim from the OP. I took it to mean something more than "have used" or "are familiar with". I took it to mean something like "has written more than one substantial project using". Did your co-workers fit into that category? Do you expect that they represent the norm of those who "specialize" in the system? I expect that most people who have written more than one substantial project using Coq work in program verification or type theory, where the name "coq" is not unusual enough that it still evokes laughter.
KERMIT also said: "Coq won't catch on in many places where it'd be very useful solely because of its name."
I am surprised by this. Are you sure? Have you witnessed this? In the laughing case or cases you mention, did the laughter turn into a rejection of the idea because of the name? Do you think Isabelle or HOL get used more often as a result?
I just expect more from technical professionals -- not that they never laugh at a silly dirty joke, but that major project decisions are based on more than programming language's name, especially in a sparse field like the one Coq is in.
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.
pascal_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 for an example.
12 comments
[ 895 ms ] story [ 1744 ms ] threadYou are really good at coq? So, what's your favorite thing about coq? Do you guys ever have coq meetups?
Naming is important.
Coq is not a general-purpose programming language. People who "specialize in this language" generally work in a field where everyone is familiar with the name "coq" and nobody bats an eye.
I think my claim that "People who 'specialize in this language' generally work in a field where everyone is familiar with the name 'coq' and nobody bats an eye." is sufficiently specific that it is not in contradiction with your anecdote. I used the word "specialize" because I was responding to a claim from the OP. I took it to mean something more than "have used" or "are familiar with". I took it to mean something like "has written more than one substantial project using". Did your co-workers fit into that category? Do you expect that they represent the norm of those who "specialize" in the system? I expect that most people who have written more than one substantial project using Coq work in program verification or type theory, where the name "coq" is not unusual enough that it still evokes laughter.
KERMIT also said: "Coq won't catch on in many places where it'd be very useful solely because of its name."
I am surprised by this. Are you sure? Have you witnessed this? In the laughing case or cases you mention, did the laughter turn into a rejection of the idea because of the name? Do you think Isabelle or HOL get used more often as a result?
I just expect more from technical professionals -- not that they never laugh at a silly dirty joke, but that major project decisions are based on more than programming language's name, especially in a sparse field like the one Coq is in.
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.
There is a reason not to panic: it can only get better, not worse...
For predicates that can be computed in coq, we can do away with the names:
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 for an example.