Bend

Bend is a systems programming language that combines native performance, automatic parallelism, and a proof-driven type system to force correctness from AI-generated code. It compiles to native binaries that approach C-level single-core speed and the same binaries scale across many cores or GPUs (CUDA) for orders-of-magnitude speedups. The type checker is also a proof checker inspired by Lean/Rocq but engineered to run in seconds so agents can re-check after every change. Parallelism is implicit: no threads, locks, or manual kernels - splitting work multiplies across CPU and GPU cores automatically. Benchmarks and demos emphasize fast compile-and-run cycles and dramatic parallel scaling (examples include pow2 on thousands of GPU cores).

Bend enforces invariants through LAWS.bend (declarative laws) and PROOF.bend (machine-checked proofs). Laws express properties that must never be violated; any change, including AI edits, must come with a proof that the laws still hold, making certain bug classes mathematically impossible to merge. The recommended workflow is to install via the provided installer, add Bend usage instructions to agents' configuration (run bend guide, keep LAWS.bend, run bend PROOF.bend before commits), and parallelize compute-heavy code. The language rests on BendTT (an affine dependent type theory) and BendRT (a parallel runtime) and is still evolving, so expect active development and to report issues.