saved
Bend
Hraness cites a source capture. The source author remains the source.
gist
Bend’s public site pitches a programming language for post-AGI vibe coding: near-C single-core speed, automatic multi-core and CUDA parallelism, and Lean-style proofs that run fast enough for an agent to check after every change. Intent is declared as laws in LAWS.bend; PROOF.bend must show they hold before commit, so AI mistakes that break those laws cannot merge. The landing page is product prose with install steps, AGENTS.md instructions, a guarded-game demo, and links to GUIDE.md plus BendTT/BendRT papers—not a long essay.
ideas
- Laws beat ambiguous prompts. Humans stop reading code but still need precise intent; laws and proofs replace fuzzy natural-language acceptance for what must never break.
- Speed is agent-shaped. Native compile near C, automatic parallel/GPU scale, and sub-second proof checking so agents can verify after each edit instead of waiting on slow dependent-type tooling.
- LAWS.bend is AGENTS.md with teeth. Declared laws make “make no mistakes” type-checked; without them a wrap-around board change can merge a broken invariant, with them the agent must repair and prove before ship.
- Young backend-first stack. Install via curl script, point agents at bend guide, LAWS, and PROOF, prefer Linux and macOS backends, and expect bugs while the language evolves.
quotes
“a fast language that blocks AI mistakes via proof”
“How can you trust code you never read? By demanding a proof.”
“Merging a bug is mathematically impossible: it is a theorem.”
“LAWS.bend is AGENTS.md backed by proof.”