{"path":"research/bend-and-deliberus/bend-hvm-status-report-2026-09-29.md","content":"<!-- Verbatim final report of the research subagent commissioned 2026-09-29 for\nbend-and-deliberus.md. Persisted unchanged from the session record (subagent a3e21059d5a24a1aa),\nper the rule that research findings are kept verbatim. The synthesis that uses it is\n../bend-and-deliberus.md. Source files it downloaded were read in the session scratchpad and are\nnot kept. -->\n\n# Bend, HVM and successors: status as of 2026-09-29\n\n[n] refers to the numbered source list at the end, which gives each URL and a read-depth tag. My operating rules allow only one verbatim quotation per response, so every other attribution is a paraphrase with the exact figures. I created or edited no project files. Source documents were downloaded to the session scratchpad and read there.\n\n## 0. Headline findings\n\n- **Two different languages now use the name Bend.**\n  - Bend 1 (May 2024) compiled to HVM2, an interaction-combinator runtime [8][12].\n  - Bend 2 (launched 2026-09-17 [19]) is a new affine, dependently typed language. Its runtime, BendRT, uses no interaction nets, and Bend 1 code does not carry over [1][3].\n- **The HVM line is separate:** HVM1 (2022, lazy, beta-optimal), HVM2 (2024, strict, GPU), HVM3 (Haskell prototype, lazy and optimal), and HVM4 (C, not launched) [13][12][14][15].\n- **Almost all benchmarks come from HOC itself.** Independent tests are few. They were unflattering for Bend 1, and those for Bend 2 are only days old.\n- **HOC's AGI bet is unverified.** It rests on SupGen/NeoGen, a symbolic search over superpositions that is proprietary and unpublished, and its ARC-AGI target has no published result [25][38][50].\n\n## 1. Bend 1 on HVM2\n\n**Language.**\n- Python-like syntax plus a Haskell-like equational syntax. Functions are pure, variables are always immutable, and there are no loops [9].\n- Iteration uses two constructs [9]:\n  - `fold` consumes a recursive datatype by replacing each constructor with an expression. `~` marks recursive fields, and state can be passed down.\n  - `bend` grows a structure from an initial state until a halting condition, recursing via `fork`.\n- Branching uses `match`, `switch`, `if` and `open`. Types are optional, and datatypes are lambda-encoded [9][10].\n- The language is affine: when a variable is used twice, the compiler inserts a duplication automatically [10].\n\n**Execution.**\n- HVM2 evaluates extended Lafont interaction combinators: seven node kinds plus variables, and ten interaction rules [12].\n- Lafont proved strong confluence. Rules act on disjoint active pairs, so the order of concurrent reductions does not matter [56]. HVM2 relies on this: total work does not depend on the order in which redexes are reduced [12].\n- On CPUs, HVM2 uses work-stealing. On the GPU it shares redexes within a block and gives each thread a shared-memory scratchpad [12].\n- It also needed a `!` flag on branching recursive calls to limit warp divergence. That flag took bitonic sort from 1,300 to 12,000 MIPS [12].\n\n**Laziness and optimality.**\n- HVM1 was lazy and beta-optimal [13].\n- HVM2 evaluates everything eagerly. It cannot handle infinite structures, and plain recursion hangs unless it is split into separate definitions, which expand lazily [12][10].\n- Taelin later wrote that HVM2 was not beta-optimal [20].\n\n**SUP and DUP.**\n- A superposition `{a b}` holds two values in one place, and operations apply to both. A duplication puts one value in two places [10].\n- Nested duplications can interfere. As a result, a function that copies its argument cannot itself be copied. The HVM2 paper's example is Church 2^2, and the bookkeeping that would fix this costs about 10x [10][12].\n\n**Limits.**\n- Backends: a Rust interpreter (sequential), a C interpreter (parallel) and a CUDA interpreter, plus C and CUDA code generators. NVIDIA only, no Metal, and Windows only via WSL [8][11].\n- Numbers are 24-bit: u24 (0 to 16,777,215), i24, and f24 (binary32 with low mantissa bits zeroed). Mixing types silently misreads the bits [10][12].\n- Memory is capped by 29-bit addresses: about 500 million nodes, or 4 GB [12][9].\n- IO covers print, input, files, and calls into C/CUDA dynamic libraries written against the HVM API [10]. There is no package manager [20].\n- Last releases: bend-lang 0.2.38 (2025-02-23) and hvm 2.0.22 (2024-08-09). The last HVM2 commit is from 2024-08-21 [17][6].\n- Licences: Bend 1 and HVM2 are Apache-2.0; HVM1 is MIT [6].\n\n## 2. Performance\n\n**HOC's claims for Bend 1.**\n- Throughput: 400 MIPS on one M3 Max thread, 5,200 MIPS on 16 threads, and 74,000 MIPS on an RTX 4090. The peak came from a shader-like tree-map [12].\n- Bitonic sort: 12.15 s on the Rust interpreter, 0.96 s on the C interpreter, 0.21 s on the RTX 4090 [8].\n- The same paper concedes [12]:\n  - about 5x slower than GHC on one thread, and up to 100x slower on loops and mutable arrays;\n  - 2–5x memory overhead from lambda-encoded datatypes;\n  - a single-core C summing loop beats thousands of HVM2 threads.\n\n**Independent tests of Bend 1.**\n- On launch day, a user ran Bend's recursive-sum example [36]:\n  - PyPy: 4.5 s. CPython: 1 min 42 s.\n  - Single-threaded Bend: still unfinished after 42 min on an i7-1270P.\n- Taelin gave three reasons: a probable bug, slower non-Apple CPUs, and two node allocations per arithmetic operation [36].\n- He also said the README's single-core figure had hit the 2^29-node limit. With 2^28 instead of 2^30 inputs it took 33.4 s on 1 core versus 2.94 s on 16 [36].\n- An unoptimised C++ loop over 2^30 took 1.7 s, the same as Bend's RTX 4090 figure [36].\n- A September 2024 test computed an 11x11 determinant by cofactors on a 4-core AMD FX-4130 [43]:\n  - Bend: over 2 h single-threaded, 20 min multi-core.\n  - Go: 22 s single-threaded, 4 s multi-core.\n- Taelin's November 2025 retrospective: it took a full RTX 4090 to beat one core of OCaml or JavaScript [20].\n\n**What benefits.**\n- Balanced recursive divide-and-conquer over trees benefits. Sequential folds and loops gain nothing [9].\n- The GPU did best on regular tree-maps with little allocation, and suffered from warp divergence on irregular recursion [12].\n- Bend 1 had no arrays [43][12].\n- Critics said MIPS hides overhead, and named 24-bit numbers, the 4 GB heap and unsound closure copying. Taelin replied that he had only claimed near-linear scaling with cores [36].\n\n**Bend 2, HOC's own numbers.**\n- BendRT paper (M4 Max, 2026-08-31) [3]:\n  - Sequential Bend takes 0.8–1.5x the time of a hand-written C twin. That twin has one C function per Bend definition, so it mirrors Bend's structure rather than being the best possible C.\n  - 16 threads give 8.8–12.1x.\n  - The integrated GPU gives up to 67x on uniform work, but is slower than 16 CPU threads on divergent work.\n  - CUDA code is present but was not measured.\n- The 2026-09-17 pin file covers 16 benchmarks [5]. By my arithmetic:\n  - sequential Bend takes 0.70–4.41x the C twin's time (hashmap is the worst case);\n  - the GPU is slower than 16 CPU threads on hashmap, lexer, queens and symreg.\n- Proof checker: 12,800 definitions in 0.295 s, against 36.2 s for Lean and 6.0 s for Rocq. On trees_400, though, Bend takes 0.61 s against Lean's 1.34 s [5].\n\n**Independent tests of Bend 2.**\n- AkitaOnRails ported two Rust tools to v2.0.16 [41]:\n  - Native build: 62 s, against 57 s for Rust. Only 0.1 s of it was checking.\n  - The runs were network-bound, and Bend was never faster on the same work.\n  - 93 lines of laws and proofs guarded a roughly 30-line allocator. They caught an injected off-by-one error that sample outputs missed.\n- A pixel-art tool port [42]:\n  - ran about 4x slower than Rust;\n  - gained about 2x on 6 threads;\n  - dropped from 3.6 min to 4.5 s per image once lists were replaced with arrays.\n- Critics say the checker benchmark compares fully annotated Bend terms with the other provers' elaboration step (unification, implicit arguments, type classes, tactics) [40].\n- The homepage demo needs 58 lines of laws and 442 lines of proof, which SPARK proves automatically [39].\n\n## 3. Status in 2026\n\n**Repositories.**\n- The original Bend repository (created 2023-08-29) is now bendlang/bend and holds Bend 2. Bend 1 moved to HigherOrderCO/Bend1 (created 2026-09-16), and HigherOrderCO/HVM now redirects to HVM1 [6].\n- Most of the roughly 23,000 stars date from Bend 1, as Taelin acknowledged [6][37].\n- bendlang/bend is Apache-2.0, primary language TypeScript. It has had 27 GitHub releases, from v2.0.8 (2026-09-18) to v2.0.34 (2026-09-29) [6].\n- The commit history was squashed at launch; Taelin cited private data and proprietary SupGen code. It was restored after criticism [37][38].\n\n**Bend 2 design.**\n- Syntax and semantics [1][2]:\n  - Python-shaped syntax with Haskell- and Lean-like semantics, affine by default.\n  - Closures can be called at most once.\n  - Termination is checked, with `@unsafe` as an opt-out. Mutual recursion is not allowed, and there is no `if`.\n  - The guide documents no `fold` or `bend` constructs.\n- Parallelism [2][3]:\n  - A parallel-call binding promises that its calls are independent and roughly equal in size.\n  - `f!(x)` sends a call to the GPU.\n  - Tasks are never rebalanced.\n- Numbers are Nat, U32 and F32 only, and floats are axiomatic [1].\n- Targets: C, Metal, CUDA, and JavaScript (single-core) [1].\n- Few effects (print, files, TCP, UDP, channels), plus foreign C and JavaScript imports and a package hub addressed by hashes [1]. The virtual heap is 8 TB, and the default Metal span is 2 GB [3].\n- Proofs:\n  - `LAWS.bend` states properties that `PROOF.bend` must prove. There are no tactics and no proof search [1].\n  - The type theory, BendTT, allows Type:Type and negative datatypes. It argues consistency from affinity and is mechanised in a Lean file of about 4,250 lines [4][7]. A text search found no `sorry` and no `axiom` declarations [7].\n- Trust in the implementation:\n  - The README says the compiler (not the kernel) is 99% AI-written and not yet audited, and that only `--verdict` uses the proven kernel [1].\n  - Taelin warned that the kernel had drifted from the formalised theory [18].\n  - Both papers state that Claude models wrote them [3][4].\n  - The GPU is used only at runtime [37].\n\n**Why interaction nets were dropped.**\n- Taelin said he \"could not make them as fast as lower-order variants on everyday hardware\" [18].\n- The BendRT paper names what was lost: optimal reduction of shared redexes [3].\n- Taelin now positions HVM for higher-order, lambda-calculus-heavy work [37].\n\n**Plans versus delivery.**\n- August 2025 plans: NeoGen program and proof search, targets including Python and HVM, and a Halloween 2025 launch [22].\n- November 2025 plans: a lazy, optimal parallel runtime and SupGen integration [20].\n- The release that shipped has none of these [1][34].\n\n**HVM3 and HVM4.**\n- HVM3 (Haskell, MIT) [14][23][24][6]:\n  - Implements the Interaction Calculus: affine lambdas, global scope, first-class dups and sups, optimal sharing.\n  - Its compiler claimed 2,400 MIPS on one core in November 2024.\n  - Its collapser inverts functions by enumerating superpositions; Taelin called this still brute force.\n  - Last commit: 2026-01-29.\n- HVM4 (C) [15][6][21]:\n  - No licence file; the README says it is pre-launch. Last push: 2026-05-30.\n  - It documents labelled SUP/DUP rules.\n  - Taelin claims it compiles superposition code with no overhead.\n- A Bend 2 demo ports an evaluator called hvm5.c [62]. I found no public HVM5.\n\n**SupGen, NeoGen and Bender.**\n- SupGen is proprietary and unpublished [37][38].\n- Taelin's claims for it:\n  - about 1000x faster than alternatives (March 2025) [28];\n  - running natively on HVM4 (September 2025) [29];\n  - about 10x better than published symbolic synthesizers (September 2026) [38].\n- Kingscrowd's summary of the Wefunder listing says NeoGen is up to 10,000x faster [45].\n- The only outside comparison I found came from the developer of Canonical, a rival prover. In January 2025 he judged SupGen weaker [44].\n- Bender is a paid proving agent. Today it is a thin wrapper around Anthropic and OpenAI models; SupGen is promised for later [34].\n\n**AGI strategy and ARC.**\n- January 2025: a $4M post-seed round at a $100M valuation to turn SupGen into a logic-based AI architecture. The target was 85% on ARC tasks at under $1 each by the end of 2025 [25].\n- March 2025 thesis: replace matrix multiplication and gradient descent with symbolic methods. About $1M remained, with runway to the end of 2026, and $300k had been spent on 256 Apple M4 machines [30].\n- Taelin reported that SupGen found one core ARC-AGI function [27].\n- No score has been published. ARC Prize 2025 (top Kaggle score 24.03%) lists no HOC entry among its winners or paper awards [50].\n\n**Company.**\n- Funding history:\n  - Seed round: $4.5M in 2023 [47][48]. A 2024 post says $4M, about 10 engineers and a 3-year runway [26].\n  - From mid-2025, HOC sought $4M at a $60M valuation for Bend 2 [49].\n  - In November 2025, Kingscrowd showed a Wefunder SAFE with $449,300 committed [45].\n  - Wefunder's indexed page showed $0 raised on 2026-07-13 [46].\n- At launch, Taelin said HOC ships without a product and has 4 humans and 25 non-human agents [18].\n- The company website still describes Bend 1 [35].\n\n## 4. Outside criticism and theory\n\n- **Proven costs of optimal reduction:**\n  - The cost of optimal parallel beta steps cannot be bounded by any elementary function of their number [51].\n  - The same holds for duplication steps in Lamping's algorithm; the authors blame its bookkeeping oracle [52].\n  - Interaction machines based on the geometry of interaction are slower in time than standard environment machines [53].\n- **Earlier parallel work:** a GPU interaction-net evaluator was slower than sequential ones on most benchmarks [54], and some nets are inherently sequential [55].\n- **HVM1 bug:** `sum (map head (tails xs))` ran in quadratic time where Haskell is linear. The issue was closed in 2024 when HVM1 was superseded [57].\n- **Community criticism:** absolute slowness [36][43]; the inherited stars and the squashed history [37]; the AI-written compiler [1][38]; verbose proofs, and whether the laws capture what the user actually intends [39][40].\n\n## 5. Published uses\n\n- **Theorem proving:**\n  - Kind, now a minimal proof checker, last pushed 2025-01-22 [16][6].\n  - SupGen's proof search, which is unpublished [38].\n  - Bend 2's own checker, which does not use interaction nets [1].\n- **Symbolic search:**\n  - Taelin's gists [31][32]:\n    - an XOR-XNOR function found in 0.0085 s, against 2.8 s for a Haskell enumerator;\n    - ADD-CARRY found in 36k interactions, against an estimated 262 million.\n  - On Stack Overflow, a commenter suggested that pruning could give Haskell similar gains [33].\n  - Third-party toy projects: an HVM4 program synthesizer limited to depth 8 by label width [60], and a NAND-circuit synthesizer [61].\n- **Academic:**\n  - A talk on HVM2 at the FProPer workshop, ICFP 2024 [58].\n  - A 2025 SE4FP workshop case study that reuses HOC's figures [59].\n- **Graph algorithms:** only HOC's own Bend 2 BFS benchmark [5].\n- **Argumentation, knowledge graphs, counterfactual evaluation:** nothing found.\n\n## Could not verify\n\n1. Any independent reproduction of HVM2's GPU figures.\n2. SupGen or NeoGen performance, and any ARC-AGI score.\n3. Whether the $100M-valuation round closed, how much money was actually invested, and HOC's current cash.\n4. Bend 2's CUDA performance, independent replication of its checker speed, and how faithfully the TypeScript checker matches the Lean model. I did not build the Lean file.\n5. HVM4's claims about compiling superpositions, and whether HVM5 exists.\n6. A Taelin remark that interaction nets survive in Bend 2's architecture. I only saw it second-hand [37].\n7. Bend 1 usage, beyond Taelin's statement that it has no significant active user base [38].\n\n## Sources (read depth)\n1. https://github.com/bendlang/bend (Bend 2 README) FULL TEXT\n2. https://github.com/bendlang/bend/blob/main/guide/GUIDE.md PARTIAL\n3. https://github.com/bendlang/bend/blob/main/paper/BendRT.pdf FULL TEXT\n4. https://github.com/bendlang/bend/blob/main/paper/BendTT.pdf PARTIAL\n5. https://github.com/bendlang/bend/tree/main/bench (runtime and checker `_pin_/apple_m4_max.txt`) FULL TEXT\n6. https://api.github.com/repos/bendlang/bend and /repos/HigherOrderCO/{Bend1,HVM1,HVM2,HVM3,HVM4,Kind} (metadata, releases, commits, licences) FULL TEXT\n7. https://github.com/bendlang/bend/blob/main/bend2/bendtt.lean PARTIAL (text search only)\n8. https://github.com/HigherOrderCO/Bend1 FULL TEXT\n9. https://github.com/HigherOrderCO/Bend1/blob/main/GUIDE.md FULL TEXT\n10. https://github.com/HigherOrderCO/Bend1/tree/main/docs (native-numbers, dups-and-sups, lazy-definitions FULL TEXT; ffi, builtins, FEATURES PARTIAL)\n11. https://github.com/HigherOrderCO/HVM2 FULL TEXT\n12. https://github.com/HigherOrderCO/HVM2/blob/main/paper/HVM2.pdf FULL TEXT\n13. https://github.com/HigherOrderCO/HVM1 PARTIAL\n14. https://github.com/HigherOrderCO/HVM3 FULL TEXT\n15. https://github.com/HigherOrderCO/HVM4 (README FULL TEXT; docs/theory/interaction_calculus.md PARTIAL)\n16. https://github.com/HigherOrderCO/Kind FULL TEXT\n17. https://crates.io/crates/bend-lang and https://crates.io/crates/hvm FULL TEXT (API)\n18. https://x.com/VictorTaelin/status/2100374221671051472 (2026-09-17) FULL TEXT\n19. https://x.com/VictorTaelin/status/2100681226143092875 (2026-09-17) FULL TEXT\n20. https://x.com/VictorTaelin/status/1985423273304473788 (2025-11-03) FULL TEXT\n21. https://x.com/VictorTaelin/status/1985320306001477783 (2025-11-03) FULL TEXT\n22. https://x.com/VictorTaelin/status/1957775213053022614 (2025-08-19) FULL TEXT\n23. https://x.com/VictorTaelin/status/1856862695028339065 (2024-11-14) FULL TEXT\n24. https://x.com/VictorTaelin/status/1858651288109465749 (2024-11-18) FULL TEXT\n25. https://x.com/VictorTaelin/status/1885328571410853951 (2025-01-31) FULL TEXT\n26. https://x.com/VictorTaelin/status/1743751536465903795 (2024-01-06) FULL TEXT\n27. https://x.com/VictorTaelin/status/1901451784943493211 (2025-03-17) FULL TEXT\n28. https://x.com/VictorTaelin/status/1897122418042286200 (2025-03-05) FULL TEXT\n29. https://x.com/VictorTaelin/status/1972292868292378821 (2025-09-28) FULL TEXT\n30. https://gist.github.com/VictorTaelin/5d42e97684ff81f7e507aa5c149b2a64 (HOC thesis, created 2025-03-02) FULL TEXT\n31. https://gist.github.com/VictorTaelin/7fe49a99ebca42e5721aa1a3bb32e278 PARTIAL\n32. https://gist.github.com/VictorTaelin/d5c318348aaee7033eb3d18b0b0ace34 PARTIAL\n33. https://stackoverflow.com/questions/78843195 SNIPPET\n34. https://bend-lang.com/ and https://bend-lang.com/bender FULL TEXT (text only; charts are images)\n35. https://higherorderco.com/ FULL TEXT\n36. https://news.ycombinator.com/item?id=40390287 PARTIAL (keyword-filtered comments)\n37. https://news.ycombinator.com/item?id=49746163 PARTIAL (keyword-filtered comments)\n38. https://news.ycombinator.com/item?id=49753179 PARTIAL (keyword-filtered comments)\n39. https://blog.liampwll.com/posts/bend_vibe_coding/ FULL TEXT\n40. https://gist.github.com/Nezk/dda0511c492cf9bd673885f0341dca0e FULL TEXT\n41. https://akitaonrails.com/en/2026/09/19/new-ai-language-just-released-bend-2/ FULL TEXT\n42. https://x.com/RealAstropulse/status/2101132976704622908 FULL TEXT\n43. https://blog.speedfox.co.uk/ (\"Breaking Bend\", 2024-09-03) PARTIAL\n44. https://leanprover-community.github.io/archive/stream/219941-Machine-Learning-for-Theorem-Proving/topic/Automated.20Math.20Prove.20Synthesizer.20without.20Deep.20Learning.html PARTIAL\n45. https://kingscrowd.com/higher-order-company-on-wefunder-2025/ FULL TEXT\n46. https://wefunder.com/higher.order.co SNIPPET (index snapshot 2026-07-13)\n47. https://news.ycombinator.com/item?id=35340472 FULL TEXT\n48. https://pitchbook.com/profiles/company/651706-84 SNIPPET\n49. https://www.linkedin.com/posts/francielle-dellamora-3579301a1_invest-in-higher-order-company-bend2-the-activity-7341469544189734913--8jZ SNIPPET\n50. https://arcprize.org/blog/arc-prize-2025-results-analysis PARTIAL\n51. https://doi.org/10.1006/inco.2001.2869 (Asperti & Mairson) SNIPPET\n52. https://doi.org/10.1016/j.ic.2004.05.001 (Asperti, Coppola, Martini) SNIPPET\n53. https://doi.org/10.1145/3434332 (Accattoli, Dal Lago, Vanoni) PARTIAL\n54. https://arxiv.org/abs/1404.0076 (Jiresch) PARTIAL\n55. https://eceasst.org/index.php/eceasst/article/download/2205/2376/2387 (Mackie & Sato) PARTIAL\n56. https://doi.org/10.1145/96709.96718 (Lafont 1990) PARTIAL\n57. https://github.com/HigherOrderCO/HVM1/issues/60 PARTIAL\n58. https://icfp24.sigplan.org/details/fproper-2024-papers/6/HVM2-Iteraction-Combinator-Evaluator FULL TEXT\n59. https://sol.sbc.org.br/index.php/se4fp/article/view/37104 PARTIAL\n60. https://github.com/Lulzx/progen SNIPPET\n61. https://dmolinad.com/projects/sym_knack/hvm_knack_circc/ SNIPPET\n62. https://github.com/bendlang/bend/tree/main/demos/pure_hvm5_mini PARTIAL\n"}