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

41–50 of 70 posts

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

#41

Post by thefz »

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.

> 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.

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

#42

Post by jonathrg »

kurtis_reed wrote: post #23
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.

What's so bad about it?

It sounds like cuck.

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

#43

Post by jroesch »

nsomani wrote: post #14
gaogao wrote: post #9

Earlier quoted context omitted.

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.

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

#44

Post by nsomani »

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 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.

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

#46

Post by 7bit »

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.

Yeah, coq is already bad, but cuq is the cherry on top of it. I don't like both.

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

#47

Post by 7bit »

antonvs wrote: post #24
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.

You know you're spending too much time on dubious sites when ...

And your low-key judging people for porn consumption in 2025.

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

#48

Post by 7bit »

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.

Then keep it and deal with the backlash without complaining.

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

#50

Post by 3836293648 »

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.

Except for the transcripts where they chose the name because they thought it was funny to offend the English
Post reply on HN