Show HN: Cuq – Formal Verification of Rust GPU Kernels

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.

Maybe this surprises you, but some people have different sensibilities than you do.

not at all - its perfectly logical

you are cucking the betabuxxed bugs in your kernels with your BFV (Big Formal Verifier)

Oh wow, honestly this caught me off guard - I've been pronouncing it "kook" in my head the whole time.

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.

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.

cuke - it's heaven in a can!

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.

There is a reason they renamed Coq to Rocq.

What's so bad about it?

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.

Take a seat in the chair

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.

It's your project, but with the current name I'd expect this thread to be duplicated any time the project is discussed.

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 suppose it depends on one's definition of "dubious sites".

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!

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.

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.