Bend
bend-lang.com- Category
- Developer Tools
- Rank
- No. 2793Tools index
Previous survey · No. 2664 ·
- Type
- TOOL
- Use case
- Coding
- GitHub
- 24.6k stars
- Latest release
- v2.0.39
- Date
About
Bend is a programming language built for AI coding agents that pairs Lean-style dependent-type proofs with a compiler generating native code that runs in parallel across CPU cores or on the GPU. Developers write invariants in a LAWS.bend file so violations are caught and blocked before an AI-written change can be merged, rather than relying on natural-language instructions alone.
What it does
A typed language where a program can carry machine-checked proofs about its own behaviour. You write down rules the app must never break, such as "balances always sum to zero", and an AI agent has to supply a proof each time it edits the code; without one, the check fails. The syntax reads like Python with types that can mention values. One source compiles to C, Metal, CUDA or JavaScript, and a function that splits its work in two gets the halves spread over every available core.
Why it's ranked here
The pitch is unusual and concrete: instead of trusting an agent to follow written instructions, make breaking a stated rule fail the check. Real depth sits behind it: Apache 2.0, two papers on its type theory and runtime, a benchmark suite pitting it against C, TypeScript and Lean, and a second checking path that rechecks proofs with a small kernel whose soundness claims are proven in Lean. The README is also unusually candid, listing more than thirty limitations. Its place rests on ambition and openness, not maturity.
What's good
The proof burden is targeted: you write a handful of rules and only those are enforced. The trusted checker is described as human-designed and audited, and kept apart from the compiler, which is mostly AI-written. A stricter verdict mode rechecks every definition against the proven kernel and reports a mismatch instead of silently passing. Telemetry is one daily version check sending only version, OS and architecture, and an environment variable switches it off. The changelog reports CPU memory for a parallel matrix benchmark dropping from 68.5 MB to 14.5 MB.
Tradeoffs
It is young and says so. Everything must be annotated and nothing is inferred. Numbers stop at natural numbers, 32-bit integers and 32-bit floats, and nothing about floating point can be proven. Strings are linked lists, so text processing is slow. There is no TLS, HTTP library, JSON or regex, no Windows support outside WSL, no debugger, profiler or REPL, and no test framework. Native compilation is slow, and the default checker has no proof of its own and may have bugs. Bend 1 programs do not carry over.
How to use it well
Best fit: back-end logic on Linux or macOS where a few rules matter enough to prove, such as account balances, in-bounds array access or game rules, and where an agent writes most of the code. Have the agent state the rules first, run the proof check before every commit, and use the stricter verdict mode before trusting a pass. Develop against the JavaScript target for quick builds, then compile natively. It is a poor fit for text-heavy services, web APIs that need TLS or JSON, or Windows machines.
Technical notes+
Per AGENTS.md, bend2/bend.ts holds the language (parser, theory, checker) and is marked human-written; bend2/comp.ts is the single compiler, emitting one C source for host and device plus a JS backend, and its header says it is mostly AI-written with bugs expected. bend2/safe.ts implements --verdict: it elaborates the checked book to BendTT text, encoding each datatype as a tag plus a Sigma chain of fields, and hands it to a Lean-built kernel; anything the kernel cannot express is marked out of scope and fails the verdict. bend2/main.ts is the CLI and doubles as a Bun plugin and Node loader so JavaScript can import Bend modules; its check() telemetry honours BEND_NO_TELEMETRY. bend2/base.bend declares File, Socket and Window handles as opaque linear laws, so programs cannot copy or forge them.
Observed
- License
- Apache 2.0
- Implementation language
- TypeScript, run with Bun; proof kernel formalized in Lean
- Compile targets
- C, Metal, CUDA and JavaScript
- Interface
- CLI that checks, runs, builds and publishes Bend files, plus a Bun plugin and Node loader for importing Bend modules from JavaScript
- Install
- Shell installer piped from curl
- Platform support
- Linux and macOS; Windows only through WSL
- Telemetry
- Daily version check sending version, OS and architecture; disabled by an environment variable
- Editor support
- Formatting-only language server in the repository
- Testing for user programs
- No test framework, per the README's limitations list
Read from README.md, LICENSE, CHANGELOG.md, AGENTS.md, bend2/main.ts, bend2/bend.ts, bend2/comp.ts, bend2/safe.ts, bend2/base.bend.
Intel on Bend
Tags
Comments (0)
No comments yet
Editorially curated, with community endorsements as a secondary signal. Corrections welcome.