bend-a-fast-language-that-blocks-ai-mistakes-via-proof

Extract — Bend (bendlang/bend README + laws/proofs docs)

URL: https://github.com/bendlang/bend
Also: https://raw.githubusercontent.com/bendlang/bend/main/guide/GUIDE.md (§ Laws and Proofs); AGENTS.md
License: Apache-2.0
Creator: Victor Taelin + team
Read via: defuddle (README); curl raw GUIDE.md / AGENTS.md

Claims

Bend 2 = dependently typed, affine language: laws (specs) + proofs (defs) + fast parallel runtime (BendRT → C/Metal/CUDA/JS). Tagline: ambiguity-free intents for AI builders.
Not Bend1/HVM2: “Bend 1 programs and HVM do not carry over.” Separate repos historically (HigherOrderCO/Bend vs bendlang/bend).
Agent workflow: human owns LAWS.bend; AI owns code + PROOF.bend; gate = bend PROOF.bend (“All terms check.”). Framed as “AGENTS.md backed by proof.”
bend PROOF.bend --safe rechecks via small BendTT kernel formalized in Lean (bend2/bendtt.lean); translation to .bendtt itself unproven — read the file; @unsafe / foreign out of scope.
No tactics / proof search; explicit terms: {==} reflexivity, %e : P rewrite motives, structural recursion as IH.
Targets: “as fast as C on CPU, as fast as CUDA on GPU”; checker “outperform every proof assistant by several OOMs” (vendor benches; see bend2.dev notes for caveats).
Compiler ~99% AI-written, not fully audited; “checker has no proof and may have bugs; --safe uses a proven kernel.”

Key workflow (GUIDE)

LAWS.bend   # human claims (AI must not edit)
PROOF.bend  # AI proofs: def Laws.<name> mirrors law <name>
bend PROOF.bend          # CI gate
bend PROOF.bend --safe   # + BendTT Lean kernel

Equality type {a == b : T}; proof when both sides compute equal. exs y: T asks for witness (y, proof). Failed step prints expected vs observed; ?TODO leaves open.

Key numbers / limits (README)

Parallel demo: pow2(20) → 4,096 GPU cores.
Numbers: Nat, U32, F32 only (no U64/I64/F64; Metal has no f64). F32 axiomatic — nothing about FP can be proven.
Affine values; closures/arrays not freely shared; + for reusable Data.
One C file / program; no separate compilation / incremental builds; no Windows (WSL ok).
Effects: print, env, time, sleep, spawn, channels, files, TCP, UDP — no TLS/HTTP/JSON/regex yet (foreigns ok).
Lean kernel build pinned Lean v4.34.0 (AGENTS.md).
Papers: paper/BendTT.pdf, paper/BendRT.pdf; formalization bend2/bendtt.lean.

Quotes

“In the post-AGI economy, humans will eventually stop writing and reading code, but we still need an ambiguity-free language to communicate our intents to the AIs… Bend is that language.”

“In short, LAWS.bend is AGENTS.md backed by proof.”

“Bend has no tactics or proof search; proving theorems takes extra effort.”

“The compiler (not kernel) is 99% AI-written and not yet fully audited. The checker has no proof and may have bugs; --safe uses a proven kernel.”

“We envision that ‘law-driven development’ will eventually become the way humans use AI to write and maintain large codebases…” (GUIDE)

DIY / fleet relevance

Natural propose → bend PROOF.bend → repair loop; keep laws human-owned.
Prefer --safe on release gates knowing translation gap + foreign/@unsafe exclusions.
Best fit: backend / Linux-macOS parallel pure compute + app laws; weak for FP-heavy, HTTP/TLS stacks, Windows-native.
Do not conflate with Bend1/HVM2 when choosing stack.

Caveats (honest README list)

Young language: verbose (no inference), no typeclasses/traits/macros beyond templates, no if-then-else (match Bool), strings = char linked lists, Base small, JS single-core, unbalanced parallelism not handled (fixed assignment), hub packages = hashes only, terse errors, no debugger/REPL/test framework beyond guide.