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.
Show HN: Cuq – Formal Verification of Rust GPU Kernels
11–20 of 70 posts
Re: Show HN: Cuq – Formal Verification of Rust GPU Kernels
#12This 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 are cucking the betabuxxed bugs in your kernels with your BFV (Big Formal Verifier)
Re: Show HN: Cuq – Formal Verification of Rust GPU Kernels
#13This 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.
Re: Show HN: Cuq – Formal Verification of Rust GPU Kernels
#14Hi 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) *…
Do you think it might be easier to target cuTile instead of PTX? (Probably not, since it has a less formalized model?)
Re: Show HN: Cuq – Formal Verification of Rust GPU Kernels
#15Re: Show HN: Cuq – Formal Verification of Rust GPU Kernels
#16This 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.
Re: Show HN: Cuq – Formal Verification of Rust GPU Kernels
#17This 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.
Just go ahead and rename this project to "Rocuda", save everyone a lot of time arguing about what names are appropriate or not.
Re: Show HN: Cuq – Formal Verification of Rust GPU Kernels
#18This 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.
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.
Re: Show HN: Cuq – Formal Verification of Rust GPU Kernels
#19This 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.
Oh wow, honestly this caught me off guard - I've been pronouncing it "kook" in my head the whole time.
Re: Show HN: Cuq – Formal Verification of Rust GPU Kernels
#20Earlier quoted context omitted.
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.
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.