bend2-vs-lean
Extract — Bend2 vs Lean
Section titled “Extract — Bend2 vs Lean”- URL: https://bend2.dev/notes/bend2-vs-lean/
- Read via: defuddle
- Companion: https://bend2.dev/notes/what-is-bend2/ ; Lean reference / mathlib
Claims
Section titled “Claims”- Both use dependent types + public native toolchains; diverge on proof authoring and execution.
- Lean: elaborates source + tactic scripts → small kernel; mathlib of lemmas/tactics.
- Bend2: explicit proofs via functions/match/equality rewrites; no tactics or proof search; safe recursion = structurally smaller input;
@unsafeoutside discipline. - BendTT paper + Lean formalization public; README documents mismatches between formalization and
bend.tsimplementation. - Same types, different jobs: Bend even-halving proof = explicit induction + rewrite motive; Lean tactics can auto-build such terms then kernel-check.
- Game demo:
LAWS.bend/PROOF.bendprove model properties (e.g. safe-position over move lists) — does not cover unmentioned requirements, JS renderer, or compiler correctness. - Execution: Bend = compiled balanced fork/join CPU+GPU; Lean = Tasks + reference counting; GPU typically foreign.
Key numbers (checker bench, upstream)
Section titled “Key numbers (checker bench, upstream)”On Apple M4 Max, synthetic checker file (12,800 definitions):
| Tool | Time |
|---|---|
| Bend | 0.295 s |
| Lean | 36.177 s |
Inputs/runner now public under bench/checker/. Caveat from note: “These four synthetic cases do not measure a port of a mathlib-dependent application, and the numbers have not been independently reproduced here.”
Side-by-side (from note)
Section titled “Side-by-side (from note)”| Requirement | Lean 4 | Bend 2 |
|---|---|---|
| Proof construction | Explicit terms or tactics | Explicit terms + rewrite motives |
| Proof reuse | mathlib + packages | Base lemmas + demos |
| Native parallel | Tasks | Balanced fork/join |
| GPU | Foreign / external pkgs | Marked ! on Metal/CUDA |
| License | Apache-2.0 | Apache-2.0 |
| Formalization | Kernel checks elaborated terms | Core formalization has documented impl mismatches |
Quotes
Section titled “Quotes”“Lean elaborates source and tactic scripts into terms checked by a small kernel; Bend instead requires explicit proofs built with its function and match syntax.”
“The theorem does not cover unmentioned requirements, the JavaScript renderer, or the compiler’s correctness.”
“Bend suits an evaluation where affine code and native CPU/GPU execution are requirements and the project can supply its own proofs. Lean supplies existing mathematical libraries and tactics that can remove substantial proof-writing work.”
“Compare a representative program and its actual library dependencies before choosing on checker timings alone.”
DIY / fleet design choice
Section titled “DIY / fleet design choice”- Choose Lean when: mathlib/tactics matter; agent already strong at Lean (Vero-style); need mature ecosystem / CI (
lake); proofs about math or software scaffolds without needing BendRT GPU. - Choose Bend2 when: product is the parallel program; laws gate AI edits; willing to write/maintain explicit proofs; accept young compiler + formalization gaps;
--safeas extra kernel pass. - Do not pick on checker OOM claims alone — proof construction cost dominates agent loops; Bend’s missing tactics may increase LLM token/repair work even if check is fast.
- Hybrid pattern (future): Lean for hard theory / audit of BendTT; Bend for shipping parallel app with LAWS gate — note does not prescribe this, but mismatch disclosure supports treating Bend checker as engineering trust, not drop-in Lean substitute.