A short introduction to Coq(coq.inria.fr)
coq.inria.fr
A short introduction to Coq
http://coq.inria.fr/a-short-introduction-to-coq
2 comments
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:
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.
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.
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.
I 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...
There is a reason not to panic: it can only get better, not worse...
Sorry, I have to ask -- it's the reddit/adolescent in me. What's the proper way to pronounce the name?
Just the way the redditing adolescent in you wants to pronounce it.
I mean, seriously, I'd never specialise in this language because everyone will turn to a teenager when you are listing your skills.
You are really good at coq? So, what's your favorite thing about coq? Do you guys ever have coq meetups?
Naming is important.
You are really good at coq? So, what's your favorite thing about coq? Do you guys ever have coq meetups?
Naming is important.
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.
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.
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.
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.
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"
"koke", or look up pronunciations for "coq al vin"
lol seriously
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.