31–40 of 70 posts
Earlier quoted context omitted.
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.
cuke - it's heaven in a can!
This is pretty cool! Are you sure about the name...
Earlier quoted context omitted.
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.
There is a reason they renamed Coq to Rocq.
Earlier quoted context omitted.
There is a reason they renamed Coq to Rocq.
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.
Earlier quoted context omitted.
There is a reason they renamed Coq to Rocq.
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.
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!
HOWEVER, I'm curious whether a proof‑driven approach like this can scale beyond toy examples or specific hardware assumptions. If so, it might set a precedent for bringing formal methods to other low‑level domains too......
Earlier quoted context omitted.
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.
There is a reason they renamed Coq to Rocq.
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.
Earlier quoted context omitted.
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.
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.…
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.