yet us french people have exactly zero problems with "bit" sounding the same than https://en.wiktionary.org/wiki/bite#French

Hah! Yes, a while ago I came up with the "fan theory" that the French named Coq as revenge for exactly that:

https://news.ycombinator.com/item?id=26739666

this, or it just comes from one of the original authors' name, Thierry Coquand ?

We _know_ it doesn’t just come from Coquand’s name, because Gérard Huet very clearly said so.

Why not? That would be a great opportunity to model adult behavior for a bunch of teenagers.

On the best of days I can make the students remember one, maybe two important points from a given lecture. The second I say Coq in class, the takeaway from that lecture is that the professor said Coq, not anything having to do with theorem proving.

For those kids, maybe that's a more important thing for them to learn? I mean, so many future encounters will be affected by their ability to not turn everything into crude sex jokes, compared to the number of circumstances where it will benefit anyone for them to know about theorem provers.

Maybe that's a bit too touchy-feely, but from a more ruthless, "only the course material matters" perspective, fine, let the kids who can't get over the name suffer the consequences. The kids who take it in stride will have an advantage. Nothing wrong with that.

It doesn't just affect the immature kids, because the immature kids affect the rest.

Call it "coke"? Plenty of people mispronounce Latex. Not the end of the world, and easier than a name change.

Isn’t that the same solution? Change the name because of how it sounds? I can’t see how that isn’t a name change.

In fact, on the list of new proposals for a successor name, a few proposals are pronounced “coke.”

Pronunciation is in fact a different thing than changing a name. If someone mispronounces my name, it doesn't mean they've given me a new name. And people that want to pronounce it coq still can.

Like how the correct pronunciation of LaTeX is "lay-tech", while obviously a lot of people pronounce it "latex".

If someone decided to start intentionally pronouncing my name wrong from now on because they don’t like how it really sounds, I’d certainly feel like they were changing my name.

Likewise for just changing the sound to “coke.” It’s a decision that the real sound sounds bad, with a suggestion to change it to a different sound. Same problem, same solution.

If the maintainers decide to change the sound or the spelling, I’ll call it whatever they want. And I’ll be more comfortable presenting it at work if it doesn’t sound like I’m saying cock.

People (usually by their native language) can't all hear and pronounce all sounds equally well.

If you can't reliably pronounce my name and it'll sound like a bad word when you try, then you should say what you can say safely. I don't care enough that I want you nervous or slowing down a meeting. But if you expect me to change my name to what you could say I would not.

You trying your best is okay, you requiring me to lower the bar so you can succeed is not okay.

That sounds like a you problem. Also, you could say "the language" for the oh-so-many times(?) you apparently have to have to refer to it during a programming class.

No because you know what happens? Students snicker and ask insincere questions just so they can say coq in class in front of their friends. They record their professor saying coq and splice it together and upload it to their social media feeds. Female students squirm in their seats and become disengaged, counting down the minutes until the class ends.

It’s the same reason I can’t teach brainfuck. There are 10001 languages worthy of class time and these languages disqualify themselves in my opinion.

How old are your students? I'm truly amazed by what you're saying.

As others mentioned, "bit" means "cock" in French, but by the time you learn what a bit is, you're old enough to not laugh at it anymore. And you surely get to use Coq in your studies when you're older than when you learn about bits.

I mean, in France, laughing at your teacher because he speaks of "bits" (cocks) and you're >16yo would certainly make you look like mentally challenged.

16 - 21. With 200 students in a room there are vast disparities in maturity levels.

Why are you trying to teach 16 year olds theorem proving? They're are no situations in which that will ever be interesting or useful to them, so it's no surprise they would be bored and distracted.

I teach a class on Programming Languages at a US university as part of an accredited CS program. The curriculum is what it is. I don't control who takes my class, and I don't restrict access to any student as long as they meet the prerequisites. At the beginning of the semester I get a roster, and I teach them the material.

For what it's worth, the 16 year old are usually the better behaved, as they are advanced students from high school who are beyond their peers in ability. They find the material eminently fascinating and are fully engaged. The ones to watch out for are the 21 year olds.

I personally learned Coq at 14. Who are you to decide what's interesting and useful to 16 year olds?

Bit is a little less niche than coq, which changes things too.

like they'd never teach you how to make coq au vin in culinary school.

Coq a l’ordinateur