what-is-bend2

Extract — What is Bend2?

• URL: https://bend2.dev/notes/what-is-bend2/
• Site: bend2.dev (independent technical notes; cites bendlang/bend @ pinned SHAs)
• Status checked in note: Bend 2.0.5 / limits as of 2026-09-20; runtime pins 2026-09-17 @ d0db7b3e
• Read via: defuddle

Claims

• Bend2 = statically typed FP language: dependent types + parallel CPU/GPU execution; programs may include compiler-checked proofs of properties before run.
• Core model: law states property; same-named def is proof. Example: cancel_idempotent on Order with {==} after match — changing Cancelled→Pending breaks proof; returning input unchanged still passes (idempotence alone ≠ “must cancel”).
• Termination: ordinary recursion must structurally descend; @unsafe bypasses and leaves proof discipline. Tail recursion → loops (no expanding native stack required).
• Affine ownership independent of app laws: plain Array<T> one owner; + / is Data for reuse; RC for shared; no tracing GC on native runtime.
• Parallelism: a b = f(x) g(y) fork/join; programmer splits; fixed assignment, no work stealing — uneven trees are author’s problem. f!(x) marks GPU (Metal/CUDA); same definition; IO stays on host.
• Effects: IO + do blocks; foreign C/JS not covered by source proofs over Bend types. “A source-level proof over Order does not verify that foreign implementation, the database… or the network.”
• Compilation: check proofs → erase types/proofs → C for BendRT or JS. Pure main evaluated by checker; IO main → JS; -o native. ./main --threads 8 --gpu off.
• Maturity: Apache-2.0; Bend1 source incompatible; HVM ≠ BendRT. Explicit proofs only (no tactics). One C file, no incremental compile. Numbers: Nat/U32/F32 only (no F64).
• Critical honesty: “mismatches between the checker and its Lean formalization”; “A correct source proof cannot compensate for a compiler bug”; “Review the laws as part of the program too; weakening a requirement makes its proof easier…”

Key numbers (upstream M4 Max runtime pins)

Workload	1 CPU thread	Parallel CPU	GPU
Game of Life	7.803 s	0.647 s	0.063 s
Lexer	2.144 s	0.198 s	1.075 s

Note: compares Bend modes only; no optimized hand CUDA baseline in that table. Checker throughput ≠ program speed ≠ proof-authoring effort.

Comparison table takeaway (Bend2 vs Lean/Rust/Mojo/…)

• Bend2 uniqueness: dependent app laws + same-source GPU ! + affine BendRT.
• Lean: tactics + mathlib; Tasks/RC; GPU via FFI.
• Rust: ownership without theorems; Rayon steals work.
• Bend1: HVM2 auto-parallel reductions; no dependent law/proof language in published syntax.

Quotes

“A program can include proofs that its functions satisfy specified properties, which the compiler checks before execution.”

“The current implementation requires explicit proof terms, with no tactic language or proof search.”

“The implementation’s limits include mismatches between the checker and its Lean formalization… A correct source proof cannot compensate for a compiler bug that changes the program’s meaning.”

“Proof-checking throughput is another measurement; it says nothing about program speed or the effort needed to construct a proof.”

DIY relevance

• Use Bend2 when you need executable verified parallel code and can accept explicit proofs + young toolchain.
• Always separate: (1) law strength, (2) checker trust (--safe + review .bendtt), (3) foreign/IO trust boundary, (4) runtime speedup measurement methodology.
• Pin revisions; note cites specific SHAs (94ee9ba…, 8008146…) — treat numbers as upstream, not independently reproduced here.