Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Show HN: Cuq – Formal Verification of Rust GPU Kernels

github.com

Post reply on HN
Print view View original

51–60 of 70 posts

Re: Show HN: Cuq – Formal Verification of Rust GPU Kernels

#51

Post by zorobo »

thefz wrote: post #41
lacker wrote: post #17

Earlier quoted context omitted.

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.

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.

Re: Show HN: Cuq – Formal Verification of Rust GPU Kernels

#52

Post by CaptainOfCoit »

ironmagma wrote: post #35
bigstrat2003 wrote: post #34

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.

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.

Re: Show HN: Cuq – Formal Verification of Rust GPU Kernels

#53

Post by matt_kantor »

CaptainOfCoit wrote: post #52
ironmagma wrote: post #35

Earlier quoted context omitted.

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.

Re: Show HN: Cuq – Formal Verification of Rust GPU Kernels

#54

Post by pwdisswordfishy »

lacker wrote: post #17
skrrtww wrote: post #8

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.

Meanwhile, nobody consulted the French when the bit was being named.

Re: Show HN: Cuq – Formal Verification of Rust GPU Kernels

#56

Post by gaogao »

jroesch wrote: post #43
nsomani wrote: post #14

Earlier quoted context omitted.

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.

Re: Show HN: Cuq – Formal Verification of Rust GPU Kernels

#58

Post by vlovich123 »

sayrer wrote: post #20
bitwize wrote: post #11

Earlier quoted context omitted.

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.

Re: Show HN: Cuq – Formal Verification of Rust GPU Kernels

#60

Post by ironmagma »

matt_kantor wrote: post #53
CaptainOfCoit wrote: post #52

Earlier quoted context omitted.

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…

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.
Post reply on HN