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.
Oh also good talk at PTC yesterday! I had meant to ask you more about the formal memory model, but the other post talk questions ended up being really interesting too.
Oh really? I can't find anything about the memory model online. I'm not sure what's the best way to do this, but if there's a way for us to get in contact, I'd be interested in adjusting the project so it's developed in the most ergonomic way possible. I'm chatting with a couple of universities and I might issue a research grant for this project to be further fleshed out, so would be keen to hear your insights prior to kicking this off. My email is neel[at]berkeley.edu.
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.
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.
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.
> 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.
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!
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.
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.
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.
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.
Coq is also named after the creator Coquand. It’s a shame that his work is being minimized because the English-speaking majority is sensitive and can’t hear a homonym for the slang for a male body part.
I wish we sometimes lived in a world where people wouldn’t be afraid at work to discuss why they like or dislike Coq or whether it meets their needs or if it’s too much for them. A man can dream though, a man can dream.
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.
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......
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.
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.
We also have a formal memory model and the program semantics are simpler so if anything reasoning about it should be easier.
Oh also good talk at PTC yesterday! I had meant to ask you more about the formal memory model, but the other post talk questions ended up being really interesting too.
Oh really? I can't find anything about the memory model online. I'm not sure what's the best way to do this, but if there's a way for us to get in contact, I'd be interested in adjusting the project so it's developed in the most ergonomic way possible. I'm chatting with a couple of universities and I might issue a research grant for this project to be further fleshed out, so would be keen to hear your insights prior to kicking this off. My email is neel[at]berkeley.edu.
[dead]
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.
> 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.
Then keep it and deal with the backlash without complaining.
Except for the transcripts where they chose the name because they thought it was funny to offend the English
Then spell the letters if the name offends you
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.
Meanwhile, nobody consulted the French when the bit was being named.
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.
That's exactly what parent said, people are overly sensitive and that's why the name had to change.
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.
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.
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!
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.
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.
What if my best friend Cunty comes to visit[1]?
[1]https://youtube.com/watch?v=Obagb7RQeYo
[flagged]
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.
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
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.
Maybe this surprises you, but some people have different sensibilities than you do.
Not the whole world speaks English. "Chicago" speaks funny in Italian, rename the city because I am offended. See how ridiculous it sounds?
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
It sounds like cuck.
Yeah, coq is already bad, but cuq is the cherry on top of it. I don't like both.
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.
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".
And your low-key judging people for porn consumption in 2025.
In 2025, we know a lot about related mental health implications.
not at all - its perfectly logical
you are cucking the betabuxxed bugs in your kernels with your BFV (Big Formal Verifier)
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.
Coq is also named after the creator Coquand. It’s a shame that his work is being minimized because the English-speaking majority is sensitive and can’t hear a homonym for the slang for a male body part.
I wish we sometimes lived in a world where people wouldn’t be afraid at work to discuss why they like or dislike Coq or whether it meets their needs or if it’s too much for them. A man can dream though, a man can dream.
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
Can we instead please be mature about choosing a adequate sounding name?
Bonus points if it runs on UNIX
I'm getting a ԃҽʝα ʋυ
[dead]
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......
As a swede I am reminded of the Honda Fitta.
Or Heinz's mayo-ketchup fusion, which had a funny translation in a local native language:
"This new sandwich spread, whatever it is, they call it Mayochup, In Cree, it means shit-face. lol"
https://www.cbc.ca/news/canada/sudbury/mayochup-cree-transla...
I wished this name had been reserved for some sort of monitoring software.
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.
Cuck?
[dead]
[flagged]
'Yer a cuq, Harry