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.
edit: According to the author in a reply, the double entendre was in fact not intentional.
Just go ahead and rename this project to "Rocuda", save everyone a lot of time arguing about what names are appropriate or not.
Which is a perfectly legitimate name in French and the whole "issue" can be worked around by spelling cee-oh-queue.
They also renamed NIPS -> NeurIPS conference, even though the name sounds less subject to jokes.
> 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.
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!
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.
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.
you are cucking the betabuxxed bugs in your kernels with your BFV (Big Formal Verifier)
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.
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.
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 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...
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.