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.
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. 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!
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.
Hi all, this is a small research prototype I built that connects Rust's MIR (Mid-level IR) to Coq, the proof assistant used for formal verification.
cuq takes the MIR dump of a Rust CUDA kernel and translates it into a minimal Coq semantics that emits memory events, which are then lined up with the PTX memory model formalized by Lustig et al., ASPLOS 2019.
Right now it supports:
* a simple saxpy kernel (no atomics)
* an atomic flag kernel using acquire/release semantics
* a "negative" kernel that fails type/order checking
The goal isn't a full verified compiler yet. It's a first step toward formally checking the safety of GPU kernels written in Rust (e.g. correct use of atomics, barriers, and memory scopes).
Happy to hear thoughts from folks working in Rust verification, GPU compilers, or Coq tooling.
Reading through this thread, it seems the naming debate is taking up most of the oxygen, but the underlying technical goal behind the project is worth highlighting. Formal verification for GPU kernels could make massively parallel Rust code safer and more reliable as more workloads move onto GPUs. Race conditions and undefined behaviors in GPU programming are notoriously tricky to reason about;
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......
It's a system where a 3rd party library (aptly named Coq) gets to throughly verify your kernel, and you get to watch it do its thing? I think the name is fitting.
Yeah, "coq" is a grade school joke in French class. It just means "rooster" or something in French, but it sounds ridiculous in English. This one has the same problem.
A company with that in the name made the French national team jersey for a while.
To be entirely fair cock (which surprisingly isn't actually derived from french but from english's germanic roots) also means rooster in english as well.
Step 1: Make sure no other programming language has the name you want.
Step 2: Make sure the name you want isn't a slur or rude word in all the languages your audience will write in. Be sure to check misspellings and homophones.
Optional 3rd step is to make sure the name lends itself to a cute animal mascot. For this project, I dunno maybe a corner chair is the mascot.
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.
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.
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.
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.
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.
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!
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.
cuke - it's heaven in a can!
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
Maybe this surprises you, but some people have different sensibilities than you do.
Oh wow, honestly this caught me off guard - I've been pronouncing it "kook" in my head the whole time.
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.
I think I've just spent too much time reading the word "CUDA" that I read "cu" as "koo", lol.
It's your project, but with the current name I'd expect this thread to be duplicated any time the project is discussed.
What's so bad about it?
Take a seat in the chair
You know you're spending too much time on dubious sites when ...
Not really, unfortunately the word hovers in the comment sections of mainstream American political discourse.
I suppose it depends on one's definition of "dubious sites".
not at all - its perfectly logical
you are cucking the betabuxxed bugs in your kernels with your BFV (Big Formal Verifier)
Hi all, this is a small research prototype I built that connects Rust's MIR (Mid-level IR) to Coq, the proof assistant used for formal verification.
cuq takes the MIR dump of a Rust CUDA kernel and translates it into a minimal Coq semantics that emits memory events, which are then lined up with the PTX memory model formalized by Lustig et al., ASPLOS 2019.
Right now it supports:
* a simple saxpy kernel (no atomics)
* an atomic flag kernel using acquire/release semantics
* a "negative" kernel that fails type/order checking
The goal isn't a full verified compiler yet. It's a first step toward formally checking the safety of GPU kernels written in Rust (e.g. correct use of atomics, barriers, and memory scopes).
Happy to hear thoughts from folks working in Rust verification, GPU compilers, or Coq tooling.
Do you think it might be easier to target cuTile instead of PTX? (Probably not, since it has a less formalized model?)
That instinct is right. cuTile would be easier to parse but harder to reason about formally.
Reading through this thread, it seems the naming debate is taking up most of the oxygen, but the underlying technical goal behind the project is worth highlighting. Formal verification for GPU kernels could make massively parallel Rust code safer and more reliable as more workloads move onto GPUs. Race conditions and undefined behaviors in GPU programming are notoriously tricky to reason about;
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......
This is pretty cool! Are you sure about the name...
It's a system where a 3rd party library (aptly named Coq) gets to throughly verify your kernel, and you get to watch it do its thing? I think the name is fitting.
It's called Rocq now—for this reason.
Yeah, "coq" is a grade school joke in French class. It just means "rooster" or something in French, but it sounds ridiculous in English. This one has the same problem.
A company with that in the name made the French national team jersey for a while.
https://en.wikipedia.org/wiki/Le_Coq_Sportif
It's Nike now, but it still has a rooster on it.
To be entirely fair cock (which surprisingly isn't actually derived from french but from english's germanic roots) also means rooster in english as well.
Aren't we more mature than this? Granted, it's the first thing I thought of as well
Bonus points if it runs on UNIX
I'm getting a ԃҽʝα ʋυ
[dead]
Two step guide to naming programming languages.
Step 1: Make sure no other programming language has the name you want.
Step 2: Make sure the name you want isn't a slur or rude word in all the languages your audience will write in. Be sure to check misspellings and homophones.
Optional 3rd step is to make sure the name lends itself to a cute animal mascot. For this project, I dunno maybe a corner chair is the mascot.
'Yer a cuq, Harry