| ▲ | skrrtww 13 days ago |
| This might be the worst named project of all time. Not funny and demonstrates an absolutely terrible impulse on the part of the author. Probably the worst way possible to advertise your project. edit: According to the author in a reply, the double entendre was in fact not intentional. |
|
| ▲ | lacker 13 days ago | parent | next [-] |
| They're renaming Coq, too, for the obvious reason. Just go ahead and rename this project to "Rocuda", save everyone a lot of time arguing about what names are appropriate or not. |
| |
| ▲ | thefz 12 days ago | parent | next [-] | | > They're renaming Coq, too, for the obvious reason. Which is a perfectly legitimate name in French and the whole "issue" can be worked around by spelling cee-oh-queue. | | |
| ▲ | 7bit 12 days ago | parent | next [-] | | Then keep it and deal with the backlash without complaining. | |
| ▲ | 3836293648 12 days ago | parent | prev | next [-] | | Except for the transcripts where they chose the name because they thought it was funny to offend the English | | | |
| ▲ | zorobo 12 days ago | parent | prev [-] | | It is legitimate indeed, and a nod to its creator T. Coquand, but better avoid recurring, useless discussions so better change the name.
The funny (for some), quirky jokes get quickly old anyway. They also renamed NIPS -> NeurIPS conference, even though the name sounds less subject to jokes. |
| |
| ▲ | pwdisswordfishy 12 days ago | parent | prev [-] | | Meanwhile, nobody consulted the French when the bit was being named. |
|
|
| ▲ | OneDeuxTriSeiGo 13 days ago | parent | prev | next [-] |
| That's not what the name is based on. The name is cu- (as in CUDA kernels) -q (as in coq/rocq). Pronounced Cuke like cucumber. |
| |
| ▲ | ironmagma 13 days ago | parent | next [-] | | There is a reason they renamed Coq to Rocq. | | |
| ▲ | bigstrat2003 12 days ago | parent | next [-] | | Yeah, because people are overly sensitive and can't bear the thought that someone might make some harmless naughty jokes. It's a completely ridiculous name change. | | |
| ▲ | ironmagma 12 days ago | parent | next [-] | | No. Conversions about it were being avoided due to being in a work context and in general. The same goes for coc (vim plugin) by the way. | | |
| ▲ | CaptainOfCoit 12 days ago | parent [-] | | That's exactly what parent said, people are overly sensitive and that's why the name had to change. | | |
| ▲ | matt_kantor 12 days ago | parent [-] | | bistrat2003 said: > people are overly sensitive and can't bear the thought that someone might make some harmless naughty jokes ironmagma could have said: > people are overly sensitive and avoid talking about Coq at work and in general Both can be motivating factors, but not necessarily. It's possible that the Coq development team doesn't care about the jokes, but they do care about people being comfortable saying the name aloud at work. | | |
| ▲ | ironmagma 12 days ago | parent [-] | | Not overly. Appropriately. Why would you risk your reputation and job to talk about a theorem prover? The pros and cons are not evenly weighted. |
|
|
| |
| ▲ | nickpsecurity 12 days ago | parent | prev [-] | | One of my coworkers uses Siri to say what they want to search for. I'm definitely not saying: "Hey, Siri, show me examples of using Coq." Then, users of search engines will add "training," "in the workplace," "visual guide," "positions," "freelance work with," etc. Everything people use with programming languages or book titles becomes inappropriate with that name. Maybe if I worked on a chicken farm it would be OK. I'm in the hotel and retail industries doing a mix of hands-on work and customer service. You'll never hear me tell my bosses I was using that on the job. Or spending hours alone with Isabelle for that matter. HOL4 & HOL Light it is! | | |
| ▲ | Dilettante_ 12 days ago | parent [-] | | God help you if you ever need to talk about some children playing with balls in the lobby, or if maintenance asks you to order more nuts. | | |
| ▲ | nickpsecurity 12 days ago | parent [-] | | That probably won't be a problem since the words have known contexts in America. Coq will bring up only two meanings in most people's minds. Of the two, rooster isn't the most, common use in many places. Far as my above examples, they were things that might lead to porn in a search engine. Especially if it's a newer product that hasn't had as much work go into preventing that as Google did. | | |
|
|
| |
| ▲ | auggierose 12 days ago | parent | prev [-] | | Yeah, and look how well that went: https://rocq-prover.org/platform When you go to the downloads, it is actually Coq again. It was a ridiculous name, yes, but that name change is even more ridiculous. Most people are still calling it Coq, past research papers are calling it Coq, and Prince is still Prince and not the symbol. |
| |
| ▲ | webdevver 13 days ago | parent | prev | next [-] | | cuke - it's heaven in a can! | | | |
| ▲ | Aloisius 13 days ago | parent | prev [-] | | I think I must pronounce cucumber differently than you. I'd expect cuke, if pronounced like cucumber would be queueck or cuck depending on which cu in cucumber you're using. However I pronounce CUDA koo-da so cuq would be pronounced perhaps like kook. |
|
|
| ▲ | Dilettante_ 13 days ago | parent | prev | next [-] |
| Maybe this surprises you, but some people have different sensibilities than you do. |
|
| ▲ | thefz 12 days ago | parent | prev | next [-] |
| Not the whole world speaks English.
"Chicago" speaks funny in Italian, rename the city because I am offended.
See how ridiculous it sounds? |
|
| ▲ | nsomani 13 days ago | parent | prev | next [-] |
| Oh wow, honestly this caught me off guard - I've been pronouncing it "kook" in my head the whole time. |
| |
| ▲ | skrrtww 13 days ago | parent | next [-] | | If this was genuinely unintentional on your part, then bless your heart and I'm sorry for assuming the worst. You might be the least morally corrupted internet user alive today. | | |
| ▲ | nsomani 13 days ago | parent [-] | | I think I've just spent too much time reading the word "CUDA" that I read "cu" as "koo", lol. |
| |
| ▲ | skavi 13 days ago | parent | prev [-] | | It's your project, but with the current name I'd expect this thread to be duplicated any time the project is discussed. |
|
|
| ▲ | kurtis_reed 13 days ago | parent | prev | next [-] |
| What's so bad about it? |
| |
|
| ▲ | 7bit 12 days ago | parent | prev | next [-] |
| Yeah, coq is already bad, but cuq is the cherry on top of it. I don't like both. |
| |
| ▲ | tracker1 12 days ago | parent [-] | | Like a similar thread... I always thought of "coq" as "co queue" in terms of as a word. "cuq" as "cook" with the cu as in "CUDA" etc. |
|
|
| ▲ | antonvs 13 days ago | parent | prev | next [-] |
| You know you're spending too much time on dubious sites when ... |
| |
| ▲ | nvader 13 days ago | parent | next [-] | | Not really, unfortunately the word hovers in the comment sections of mainstream American political discourse. | | | |
| ▲ | 7bit 12 days ago | parent | prev [-] | | And your low-key judging people for porn consumption in 2025. | | |
| ▲ | antonvs 11 days ago | parent [-] | | In 2025, we know a lot about related mental health implications. |
|
|
|
| ▲ | webdevver 13 days ago | parent | prev [-] |
| not at all - its perfectly logical you are cucking the betabuxxed bugs in your kernels with your BFV (Big Formal Verifier) |
