A short introduction to Coq • Hacker News Board

Re: A short introduction to Coq

#11

Post by KERMIT » Wed, May 26, 2010, 11:17 PM UTC

jbapple wrote: post #10

maxklein wrote: post #9

Earlier quoted context omitted.

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.

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.

Re: A short introduction to Coq

#12

Post by pook » Wed, May 26, 2010, 11:21 PM UTC

KERMIT wrote: post #11

jbapple wrote: post #10

Earlier quoted context omitted.

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"

Re: A short introduction to Coq

#13

Post by jbapple » Thu, May 27, 2010, 3:39 AM UTC

KERMIT wrote: post #11

jbapple wrote: post #10

Earlier quoted context omitted.

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.

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.