Bend language release – fast CPU/GPU compilation with AI‑proofed laws

What Bend claims to deliver

Bend promises three core benefits:

Native‑speed execution – compiled binaries run on a single CPU core almost as fast as C, and on 16 cores or a GPU can be up to 124× faster.
Instant proof checking – the type checker is a proof checker that validates user‑defined laws in under a second, far quicker than Isabelle, Agda, Lean or Coq on comparable codebases.
Automatic parallelism – no explicit threading or kernel code is required; the runtime spreads work across all available CPU cores or GPU cores and joins the results automatically.

These claims are demonstrated on the Bend website with benchmarks (Game of Life, pow2, etc.) and a short demo that blocks an AI‑generated bug using a law that "winning is impossible".

Fast compilation and execution

Bend compiles to native machine code. On an Apple M4 Max processor the reported runtimes are:

1 core: 7.80 s (≈1× C’s 6.78 s)
16 cores: 0.65 s (≈12× speedup)
GPU: 0.06 s (≈124× speedup)

The site compares these numbers to TypeScript (18.8 s), Lean (13.8 s) and C (6.78 s). The GPU benchmark runs the same binary on 4,096 GPU cores, showing the runtime’s ability to exploit massive parallelism without user‑written kernels.

Proof‑based "laws" to block AI mistakes

Bend introduces LAWS.bend, a file where developers declare invariants that must never be violated. When an AI agent (e.g., Claude) generates code, the compiler checks the generated PROOF.bend against the declared laws. If a law would be broken, the compilation fails and the AI must retry until it produces a proof that the law holds.

Example law (no winning sequence):

# LAW: no move sequence leads to victory.
law you_cant_win:
  for moves: List<Move>
    board = replay(start(), moves)
    is_won(board) == False{}

A corresponding proof must be supplied in PROOF.bend:

# PROOF: you_cant_win holds.
def Laws.you_cant_win(moves):
  # ... AI‑generated proof

The system treats the law as a type; any code that would violate it is rejected at compile time.

Parallel runtime (BendRT)

BendRT is the runtime that automatically distributes pure functional calls across available cores. The language requires no explicit thread creation, lock management, or CUDA kernel authoring. Work is split, executed in parallel, and the results are joined transparently. The demo shows a pow2.bend program running on 4,096 GPU cores with a single command.

Community reaction on Hacker News

Praise and curiosity

Users appreciate the novel combination of fast native compilation with formal verification aimed at AI‑generated code.
Some see potential for invariant‑driven development in domains like scheduling or contract enforcement.

Skepticism and practical concerns

Proof effort: Several commenters note that writing the necessary laws and proofs can be labor‑intensive. One user reported needing ~60 lines of basic arithmetic lemmas for a simple calendar‑cron job.
Tooling gaps: Questions were raised about how the system integrates with existing libraries, whether the proofs can be reused across projects, and how to handle missing or incorrect laws.
Repository transparency: The GitHub repo shows a single recent commit and no visible commit history, leading to doubts about project maturity and trustworthiness.
Performance limits: Some observers compare Bend’s GPU performance to specialized languages like Futhark and note that balanced recursive workloads suit Bend, while dense array kernels may lag.
Enforcement guarantees: Users ask what prevents an LLM from simply ignoring a law; the answer is that the compiler will reject any generated code that does not provide a valid proof, but the AI must still be guided to produce such proofs.

Notable quotes

"LAWS.bend is AGENTS.md backed by proof. ‘Make no mistakes’ is now type‑checked." – Bend website

"The law I most wanted: ‘no two output plans overlap.’ I didn’t state it. It needs the sortedness of collapse’s input as a hypothesis… that's the honest measure of the gap between ‘provable in principle’ and ‘provable this afternoon.’" – svachalek

"20K stars and a single commit an hour ago? How many goats were sacrificed?" – plastic041 (expressing concern over repo history)

How to get started

Install with a single script:

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

Add guidance to AGENTS.md so AI agents know to run the guide, use laws, and invoke the proof checker before committing.
Write laws for critical invariants, then let the AI generate code and accompanying proofs.
Run the compiled binary on CPU or GPU; the runtime will parallelize automatically.

Open questions and future work

Scalability of proofs: How does Bend handle extremely large state spaces where enumerating all move sequences is infeasible?
Interoperability: Will Bend provide FFI bindings to call into existing C/Rust libraries, or a way to embed Bend code in larger projects?
Tooling maturity: The community is asking for changelogs, versioned releases, and a clearer commit history to build trust.
Benchmarking: Independent performance measurements (e.g., on the Bells benchmark suite) would help validate the claimed speedups.

References

Guide: GUIDE.md in the repository (full language spec).
BendTT paper: Affine dependent type theory underlying the language.
BendRT paper: Description of the parallel runtime for CPUs and GPUs.

Bend is a very early project; expect bugs and rapid iteration. Contributions and issue reports are welcomed via the GitHub issue tracker.