Bend

Bend is a programming language built around laws and proofs: you write rules your application must never break, and the compiler forces any code change to carry a mathematical proof that those rules still hold. It's aimed at developers who use AI agents to write code and want a way to catch broken invariants without reading every diff. The syntax reads like Python with dependent types added, and programs compile to C, Metal, CUDA, or JavaScript, with the whole language able to run on the GPU.

The pitch is specific: instead of trusting an AI-written pull request on faith, you declare invariants in a LAWS.bend file ("the sum of balances must be zero", "winning is impossible", "array_set() may never be called out-of-bounds"), and the AI has to write a PROOF.bend that the compiler checks. If the proof doesn't hold, the change doesn't pass. This turns "make no mistakes" from a hope into something the compiler enforces.

Key features

• Law-backed correctness: declare invariants in LAWS.bend and require compiler-checked proofs (PROOF.bend) before code changes are accepted.
• Fast native compilation: targets aim to match hand-written C on a single core and outperform it across many cores or on the GPU.
• Fast type/proof checking: the compiler checks proof files that other proof assistants (Isabelle, Agda, Lean, Rocq) take much longer to verify.
• Automatic parallelism: recursive divide-and-conquer code is spread across CPU cores or thousands of GPU cores without threads, locks, or manual kernel writing.
• Multiple compile targets: outputs C, Metal, CUDA, and JavaScript from the same source.
• Dependent type system: types can express and enforce arbitrary logical properties, not just shapes of data.
• AI-agent workflow built in: a suggested AGENTS.md snippet tells coding agents to learn Bend, maintain laws, and prove code before committing.

Ideal use cases

Bend fits projects where you're using AI coding agents heavily and want a hard backstop against regressions in specific, statable invariants: game rules, financial balance checks, bounds checks, sorting correctness, and similar properties that can be phrased as a logical statement. It also suits people experimenting with fast, parallel, GPU-targeted code without hand-writing CUDA or Metal kernels, and people interested in practical, fast proof checking compared to traditional proof assistants.

It is not a good fit yet for production systems that need mature tooling: there's no test framework, no debugger or profiler, terse error messages, no package versions or search (the hub only has hashes), and limited editor support (formatting plus a community LSP for diagnostics/hover, no completion). It also isn't suited for text-heavy processing (strings are linked lists, so slow), for code needing 64-bit numeric types, for anything requiring Windows without WSL, or for teams that need type classes, traits, macros, or automated proof tactics. Bend itself calls out that the compiler is young, 99% AI-written, and not yet fully audited, and that the Lean formalization and the implementation can mismatch, so treat it as experimental rather than something to bet a production system on outright.

Installation

Install the bend CLI directly:

curl -fsSL https://bend-lang.com/install.sh | sh

This installed bend ignores a project's bunfig.toml and .env, which matters if you're checking untrusted code; running from a source checkout via bun bend2/main.ts reads those files instead.

To wire it into an AI coding workflow, add the following to your AGENTS.md:

When using Bend:
- run `bend guide` to learn it
- use `LAWS.bend` to keep important rules
- run `bend PROOF.bend` before committing
- parallelize the code whenever possible

After that, you can just tell your agent "use Bend" and it picks up the workflow. Native compilation needs clang 14+ (19+ for the ! GPU operator), and Metal or CUDA 12 if you're targeting GPUs. On Linux, windowing and audio features need X11 and ALSA headers; there's no native Windows support, though WSL works. Bend works best on the back end, on Linux or macOS. For faster iteration during development, compiling to JavaScript is quicker than the native C/CUDA/Metal targets, though the JS target runs on a single core and has no graphics or audio support.