frontpage.
newsnewestaskshowjobs

Made with ♥ by @iamnishanth

Open Source @Github

fp.

Show HN: Cuq – Formal Verification of Rust GPU Kernels

https://github.com/neelsomani/cuq
39•nsomani•6h ago•30 comments

Show HN: Create interactive diagrams with pop-up content

https://vexlio.com/features/interactive-diagrams-with-popups/
34•ttd•11h ago•0 comments

Show HN: Onetone – A PHP full-stack framework with AI runtime, ORM, CLI

3•wowowoasdf•1h ago•2 comments

Show HN: Cadence – A guitar theory app

https://cadenceguitar.com/
173•apizon•1w ago•76 comments

Show HN: Subway Surfers in Your Terminal

https://github.com/evanreilly/homebrew-subway-surfers
6•civilchaos•4h ago•2 comments

Show HN: Modshim – A new alternative to monkey-patching in Python

https://github.com/joouha/modshim
103•joouha•6d ago•30 comments

Show HN: Katakate – Dozens of VMs per node for safe code exec

https://github.com/Katakate/k7
118•gbxk•1d ago•50 comments

Show HN: Maktabah Islam ELKIRTASS being revived on Qt6 CMake

https://github.com/abdulbadii/elkirtasse-on-Qt6-Cmake
5•dogol•5h ago•0 comments

Show HN: ProxyBridge redirect any Windows TCP/UDP traffic to HTTP/SOCKS5 proxies

https://github.com/InterceptSuite/ProxyBridge
4•anof-cyber•5h ago•0 comments

Show HN: Run any GitHub Action locally from your Cron job -- finally!

https://docs.dagu.io/features/executors/github-actions#basic-usage
22•yohamta•21h ago•0 comments

Show HN: SerenDB – A Neon PostgreSQL fork optimized for AI agent workloads

https://github.com/serenorg/serendb
6•taariqlewis•6h ago•1 comments

Show HN: bbcli – A TUI and CLI to browse BBC News like a hacker

https://github.com/hako/bbcli
78•wesleyhill•3d ago•15 comments

Show HN: ASCII Automata

https://hlnet.neocities.org/ascii-automata/
99•california-og•5d ago•10 comments

Show HN: Stopping Extreme Withdrawal – Free AI guide for extreme anxiety

https://docs.google.com/document/d/e/2PACX-1vSsyN1Qem0Qkb4dE1XsWcOcndRqnI5COunCzc7UTawH-r1TSHWHxr...
6•ycosynot•3h ago•1 comments

Show HN: Middlerok – reduces front end-back end integration from weeks to hours

https://www.middlerok.com/
2•rokontech•8h ago•0 comments

Show HN: I'm making a detective game built on Wikipedia

https://detective.wiki/
305•jasonsmiles•5d ago•43 comments

Show HN: AutoLearn Skills for self-improving agents

https://www.autolearn.dev
27•toobulkeh•23h ago•11 comments

Show HN: I created a cross-platform GUI for the JJ VCS (Git compatible)

https://judojj.com
139•bitpatch•2d ago•43 comments

Show HN: Playwright Skill for Claude Code – Less context than playwright-MCP

https://github.com/lackeyjb/playwright-skill
179•syntax-sherlock•2d ago•43 comments

Show HN: Cont3xt.dev – Universal Team Knowledge for AI Coding Tools

https://cont3xt.dev
3•ksred•9h ago•3 comments

Show HN: RuleHunt – TikTok for Cellular Automata

https://rulehunt.org
14•irgolic•10h ago•8 comments

Show HN: GuardianScan – Website audits for 2025 web standards

https://guardianscan.ai
2•buildwithnumen•10h ago•0 comments

Show HN: UHOP – Escaping Nvidia Lock-In with an Open Hardware Optimization Layer

https://www.uhop.dev/
3•danielbisina•11h ago•0 comments

Show HN: UHOP – An Open Hardware Optimization Platform for GPUs

https://github.com/sevenloops/uhop
3•danielbisina•11h ago•0 comments

Show HN: Incremental JSON parser for streaming LLM tool calls in Ruby

https://www.aha.io/engineering/articles/streaming-ai-responses-incomplete-json
12•hotk•6h ago•0 comments

Show HN: Timeplus Proton 3.0 – First vectorized streaming SQL engine

https://github.com/timeplus-io/proton
10•gangtao•11h ago•10 comments

Show HN: I'm rewriting a web server written in Rust for speed and ease of use

https://ferron.sh/
68•dorianniemiec•1d ago•90 comments

Show HN: SierraDB – A Distributed Event Store Built in Rust

https://tqwewe.com/blog/building-sierradb/
24•tqwewe•1d ago•2 comments

Show HN: caniscrape – Analyze anti-bot protections before scraping (CLI and Web)

https://github.com/ZA1815/caniscrape
3•Crroak•12h ago•2 comments

Show HN: Pong Wars Idle Game

https://verse8.io/P4s6w3C
5•wancomplete•19h ago•1 comments
Open in hackernews

Show HN: Cuq – Formal Verification of Rust GPU Kernels

https://github.com/neelsomani/cuq
39•nsomani•6h ago

Comments

nsomani•6h ago
Hi 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)

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

gaogao•4h ago
Do you think it might be easier to target cuTile instead of PTX? (Probably not, since it has a less formalized model?)
nsomani•4h ago
That instinct is right. cuTile would be easier to parse but harder to reason about formally.
Hexigonz•5h ago
This is pretty cool! Are you sure about the name...
NitpickLawyer•5h ago
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.
bitwize•4h ago
It's called Rocq now—for this reason.
sayrer•3h ago
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.

OneDeuxTriSeiGo•1h ago
To be entirely fair cock (which surprisingly isn't actually derived from french but from english's germanic roots) also means rooster in english as well.
CaptainOfCoit•4h ago
I'm getting a ԃҽʝα ʋυ
hnuser123456•4h ago
Bonus points if it runs on UNIX
skrrtww•4h ago
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.

Dilettante_•4h ago
Maybe this surprises you, but some people have different sensibilities than you do.
webdevver•4h ago
not at all - its perfectly logical

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

nsomani•4h ago
Oh wow, honestly this caught me off guard - I've been pronouncing it "kook" in my head the whole time.
skrrtww•3h ago
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.
nsomani•3h ago
I think I've just spent too much time reading the word "CUDA" that I read "cu" as "koo", lol.
skavi•1h ago
It's your project, but with the current name I'd expect this thread to be duplicated any time the project is discussed.
OneDeuxTriSeiGo•4h ago
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.
webdevver•3h ago
cuke - it's heaven in a can!
spartanatreyu•4m ago
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
ironmagma•2h ago
There is a reason they renamed Coq to Rocq.
Aloisius•1h ago
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.

lacker•3h ago
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.

kurtis_reed•2h ago
What's so bad about it?
kelseyfrog•1h ago
Take a seat in the chair
antonvs•2h ago
You know you're spending too much time on dubious sites when ...
nvader•2h ago
Not really, unfortunately the word hovers in the comment sections of mainstream American political discourse.
antonvs•34s ago
I suppose it depends on one's definition of "dubious sites".
thrownawaysz•4h ago
'Yer a cuq, Harry
ModernMech•1h ago
Two step guide to naming programming languages.

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.