4 ms·

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.

webdevver 1y ago
cuke - it's heaven in a can!
- spartanatreyu 1y ago
  For anyone who doesn't understand the reference, it's from the IT Crowd and the entire episode is on youtube: https://www.youtube.com/watch?v=VuTMphDrc4A https://www.youtube.com/watch?v=VuTMphDrc4A
ironmagma 1y ago
There is a reason they renamed Coq to Rocq.
- bigstrat2003 1y ago
  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 1y ago
    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 1y ago
      That's exactly what parent said, people are overly sensitive and that's why the name had to change.
      - matt_kantor 1y ago
        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 1y ago
        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 1y ago
    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_ 1y ago
      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 1y ago
        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.
        Dilettante_ 1y ago
        What if my best friend Cunty comes to visit[1]? [1]https://youtube.com/watch?v=Obagb7RQeYo https://youtube.com/watch?v=Obagb7RQeYo
        dekerklas 1y ago
        [flagged]
- auggierose 1y ago
  Yeah, and look how well that went: https://rocq-prover.org/platform 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.
Aloisius 1y ago
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.

webdevver 1y ago

cuke - it's heaven in a can!

spartanatreyu 1y ago
For anyone who doesn't understand the reference, it's from the IT Crowd and the entire episode is on youtube: https://www.youtube.com/watch?v=VuTMphDrc4A https://www.youtube.com/watch?v=VuTMphDrc4A

ironmagma 1y ago

There is a reason they renamed Coq to Rocq.

bigstrat2003 1y ago
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 1y ago
  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 1y ago
    That's exactly what parent said, people are overly sensitive and that's why the name had to change.
    - matt_kantor 1y ago
      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 1y ago
        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 1y ago
  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_ 1y ago
    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 1y ago
      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.
      - Dilettante_ 1y ago
        What if my best friend Cunty comes to visit[1]? [1]https://youtube.com/watch?v=Obagb7RQeYo https://youtube.com/watch?v=Obagb7RQeYo
      - dekerklas 1y ago
        [flagged]
auggierose 1y ago
Yeah, and look how well that went: https://rocq-prover.org/platform 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.

Aloisius 1y ago

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.