Bend – A language that blocks AI mistakes via proof, on CPU and GPU

	Bend – A language that blocks AI mistakes via proof, on CPU and GPU(bend-lang.com)
	591 points by nicolas-siplis 26 days ago \| 302 comments
	tl;dr: Bend is a programming language with Python-like syntax that compiles to fast native code, runs in parallel across CPU cores and GPUs, and includes a Lean/Rocq-style proof checker fast enough to run on every AI code change. Its key pitch is a `LAWS.bend` file where developers declare invariants that AI-generated code must mathematically prove it doesn't violate before committing, aimed at making "vibe-coded" apps trustworthy without human code review. It's early-stage, back-end focused, and works on Linux/macOS.
	HN Discussion: ↓AIs won't reliably follow the LAWS or will modify them to bypass constraints ~The standard library of proofs is too sparse, requiring users to prove basic facts themselves ↓Suspicious metrics (stars vs forks/issues) suggest the project's popularity is inflated or untrustworthy ↑Technically interesting language design combining QTT and staging, worth exploring further ↓Humans still need to write and validate the laws, so vibe-coding trust problem isn't solved