[jbapple]

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.