{"path":"research/bend-and-deliberus.md","content":"# Bend and Deliberus\n\n**Date**: 2026-09-29 · **Type**: research, read against the corpus · **Status**: nothing here is\nruled. One ledger row (T4) and two work items (`TODO.md`).\n\n**Occasion.** The founder, VERBATIM: *\"Also look into the Bend programming language. Perhaps that\ncould help Deliberus in various ways. Read up deeply about it and relate it to different aspects\nand levels of analysis of Deliberus and all its parts and what Deliberus vision is.\"*\n\n**Sources.** The facts about Bend come from a research pass kept verbatim in\n[bend-and-deliberus/bend-hvm-status-report-2026-09-29.md](bend-and-deliberus/bend-hvm-status-report-2026-09-29.md),\nwith its read-depth tags and 62 numbered sources. The measurement in § 4 is\n[bend-and-deliberus/measure_order.py](bend-and-deliberus/measure_order.py), run read-only against the\nlive graph on 2026-09-29, result in `order_result_2026-09-29.json` beside it.\n\n---\n\n## 0. Answer first\n\n**Do not adopt Bend.** Deliberus spends its time on model calls and database round trips, and Bend\nspeeds up neither; and the current Bend launched on 2026-09-17, with a compiler its own README calls\n99% AI-written and unaudited, from a company that reported four people at launch. The success prior names maintenance as what\nkills this whole class of project, and a young language is the largest maintenance risk available.\n\n**Four ideas from its lineage are worth taking, each as a practice rather than a dependency:**\n\n1. **Confluence** (from the original Bend's runtime): the graph should come out the same whatever\n   order its sources and passes arrive in. Measured today, it does not: 59% of auto-connect's\n   candidate pairs depend on which source came second (§ 4). The fix is cheap and the principle is\n   one the corpus already ruled for contributions.\n2. **Laws** (from the new Bend): state the properties the deterministic core must satisfy and check\n   them automatically. Sampling is how a model's judgments get proven; laws are how code does\n   (§ 5). This joins the reliability question: the checkable parts of a split can be held to a law\n   in code rather than a sample.\n3. **A small trusted kernel** (the new Bend's design, and the corpus's own Lean analogy): the new\n   Bend trusts only a small kernel and treats its large AI-written compiler as untrusted. That is the corpus's model of\n   machine passes as proposers and deterministic rules as the kernel, now tested in public, and its\n   critics found the same limit the corpus names (§ 5).\n4. **Resources that must not be used twice** (from the new Bend's affine types): one piece of\n   evidence reachable along several paths is the same problem, and separation logic's answer,\n   fractional shares that sum to one, is what the unadopted fair-share routing already does (§ 6).\n\n**At the level of the vision**, the company's bet on artificial general intelligence is symbolic\nprogram search, and search needs a specification to search against. In deliberation the\nspecification is the thing in dispute. So if that bet wins, the harness conviction predicts the same\nresidue for people that it predicts today (§ 7).\n\n---\n\n## 1. What Bend is, as of 2026-09-29: two languages with one name\n\n- **Bend 1** (May 2024) is a pure functional language with Python-like syntax that compiled to\n  **HVM2**, a runtime evaluating *interaction combinators*: programs as graphs rewritten by local\n  rules. Its two signature constructs were `bend`, which grows a recursive structure from a seed,\n  and `fold`, which collapses one into a value. Anything that could run in parallel did, on CPU\n  threads or an NVIDIA GPU, with no annotations. Numbers were 24-bit, memory capped near 4 GB.\n- **Bend 2** (launched 2026-09-17) is a new language under the same name: affine by default (a value\n  is used at most once), dependently typed, with a proof layer (a `LAWS` file states properties, a\n  `PROOF` file proves them, no tactics), compiling to C, Metal, CUDA and JavaScript through a new\n  runtime that uses **no interaction nets**. Bend 1 code does not carry over.\n- **Why the change**, in its author's words: he *\"could not make them as fast as lower-order variants\n  on everyday hardware.\"* What was given up is optimal sharing of repeated work.\n- **Performance, independently measured.** Bend 1 was slow on one core (its own paper: about five\n  times slower than Haskell's compiler, up to a hundred times on loops) and needed a high-end GPU to\n  beat one core of OCaml or JavaScript, by its author's own retrospective. Of Bend 2's first\n  independent ports, one ran about four times slower than Rust and another was never faster on the\n  same work.\n- **The company's larger bet** is SupGen, a symbolic program search over *superpositions* (several\n  alternative values held in one place). It is proprietary and unpublished, and its public target of\n  85% on the ARC abstract-reasoning benchmark by the end of 2025 has no published result.\n- **No published use** touches argumentation, knowledge graphs or counterfactual evaluation.\n\n---\n\n## 2. Level one: where Deliberus spends its time\n\n**No speedup is available here.** Bend accelerates pure computation that splits into independent\npieces. Deliberus's measured costs are elsewhere:\n\n- A ten-minute spoken segment took about twenty minutes to extract on the Claude backend, almost all\n  of it in 78 model calls (2026-09-09).\n- The similarity search was slow for months, and the stage breakdown showed the arithmetic was about\n  1% of the cost: fetching and parsing embeddings took 15 seconds, the cosine 0.19. Moving the search\n  into FalkorDB took it to 0.31 seconds in total (2026-08-17).\n- The strength calculation is a recursive walk over a few thousand claims.\n\nA faster evaluator for the walk would shave milliseconds off a request that waits on a database, and\non the production host a GPU evaluator would compete with the embedding server for its only GPU. Neither is\nworth a new language.\n\n---\n\n## 3. Level two: the algorithms have Bend's shape, which is an old shape\n\n- **Decomposition then strength is `bend` then `fold`.** The descent grows a tree of parts from a\n  claim; the strength calculation collapses it to a number. Functional programming has called this\n  pair an unfold and a fold, and their composition a *hylomorphism*, since Meijer, Fokkinga and\n  Paterson (1991). Bend 1 made it syntax; the pattern is general, and Deliberus already has it.\n- **Sharing is where Bend's runtime was clever, and Deliberus does it by hand.** A claim can be a part\n  of two parents, so the decomposition structure is a graph with shared children, not a tree. HVM's\n  selling point was computing shared work once without being told. The strength walk memoizes\n  shared children explicitly, which is the same economy.\n- **Superposition would suit counterfactual questions.** The hinge score asks, for each claim, how\n  much the root moves if that claim is granted and if it is denied: two evaluations per claim, most\n  of their work shared. A superposing runtime computes the shared part once. Elegant, and not needed:\n  nothing suggests the hinge is a bottleneck at the corpus's size, and if it became one, caching the\n  shared subtrees in Python is the ordinary fix.\n\n---\n\n## 4. Level three: confluence, and a measured order-dependence\n\n**The one deep idea in Bend 1's runtime is strong confluence.** Lafont proved that interaction\ncombinators reduce to the same result whatever order the local rewrites happen in, because each\nrewrite touches only its own pair of nodes. That is what let HVM2 run rewrites in parallel with no\ncoordination.\n\n**Deliberus's graph is also built by local rewrites** (extract, link, split, supersede, merge),\napplied by several passes in whatever order sources and people arrive. The confluence question for\nit is: **would the same sources, arriving in a different order, produce the same graph?** Where the\nanswer is no, two runs over one corpus disagree, and passes running side by side can race.\n\n**Measured read-only 2026-09-29, it is often no.** Auto-connect compares each claim of a newly\narrived source with its five most similar claims from other sources, above a similarity of 0.65. A\npair is therefore judged only if it made the top five **from the later source's side**. Computing\neach source as if it had arrived last:\n\n| | |\n|---|---|\n| Candidate pairs between extracted claims | 1,729 |\n| Reachable from both sides | 712 |\n| Reachable from one side only | **1,017 (59%)** |\n| Highest similarity among one-sided pairs | **0.778** (none reach 0.78) |\n\nSo for 59% of the pairs, whether auto-connect ever judges them depends on which of the two sources\ncame second. **None reaches 0.78**, the lowest band the sameness sitting samples, so the\nnear-duplicates that matter for sameness are safe; the exposure is supports and attacks in the middle\nband (the one-sided pairs' median similarity is 0.67). Two order-independent alternatives exist: judge\na pair when **either** side ranks it (the union, about 40% more cosine candidates, estimated from the\ncounts), or only when **both** do (mutual top five, fewer pairs, losing the one-sided ones). Ledger\nrow T4 proposes the property; `TODO.md` holds the fix and a shuffle test that ingests the stress suite\nin two orders and compares the graphs.\n\n**The same measurement sized a cost named in a concurrent proposal**, that only the keeper should\nwrite resemblance links ([auto-connect-upgrade.md](auto-connect-upgrade.md) § 2c): all 13\ncross-source pairs of extracted claims at cosine 0.80 or above sit in both claims' top five, so none\nwould lose its link, but 16 more involve a claim kind the candidate pool never admits, 9 of them\nminted reports (`measure_high_similarity_reach.py` beside this doc).\n\n**The corpus already ruled this property for contributions.** *Contributions are added, never\noverwritten* is confluence stated for people: additions commute, overwrites do not, and an edit war is\nexactly a non-confluent system, where the result depends on who acted last. It also marks where the\ncode breaks the property today: the split panel's *Save wording* overwrites a part's text in place\n([split-review-and-the-founders-intentions.md](split-review-and-the-founders-intentions.md) § 4a).\n\n**The honest limit.** Model passes are not deterministic, so exact confluence is unavailable. The\nachievable form is confluence up to recorded verdicts: when every judgment is stored with the pass\nand version that made it (ledger R8's watermark), rebuilding the graph from the same sources and the\nsame verdicts gives the same graph, and a changed verdict is an explicit event rather than an\naccident of arrival.\n\n---\n\n## 5. Level four: laws for code, samples for judgments, and a small kernel\n\n**Bend 2's proof layer supplies the clearest outside illustration of the reliability question.** In\none independent port, 93 lines of laws and proofs guarding a roughly 30-line allocator caught an\ninjected off-by-one error that sample outputs missed. A law rules out a whole class of error; a\nsample only bounds its rate.\n\n**So the two kinds of proof divide Deliberus between them:**\n\n- **Deterministic code gets laws.** The strength calculation has properties that should hold for\n  every graph: adding parts that follow from existing ones never raises a parent (the padding\n  ruling), a stronger supporter never lowers its target, recomputing gives the same answer, the order\n  edges were inserted in does not matter, fair-share evidence routing conserves each fact's total\n  weight. Some of these are pinned today by single examples (three parts and twelve parts scoring\n  identically). Property-based tests state them over randomly generated graphs; a proof assistant\n  could prove the core ones outright. `TODO.md` holds the property tests.\n- **Model judgments get samples**, as [proving-a-pass-reliable.md](proving-a-pass-reliable.md) sets\n  out, because there is no law to state for *\"is this a faithful split?\"*\n- **The checkable part of a judgment can get a law.** The splitter's contract is that it separates\n  content already in the sentence and adds none. So a part may not contain a number, a date or a\n  proper name absent from its parent. That check is deterministic, cheap, and has a known blind spot\n  (invention that uses no new names, numbers or dates), which makes it a law backing the model-based\n  coverage check rather than replacing it. `TODO.md` holds it with the splitter's proof work.\n\n**The small kernel.** The corpus already holds this analogy from Lean: a small trusted checker and a\ncreative proposer layer, with a table of what a Deliberus kernel can check (form, relevance,\nconsistency, circularity) and what needs people (truth, importance, whether a definition captures its\nconcept) ([lean-deliberus-analogies.md](lean-deliberus-analogies.md)). Bend 2 is a live instance of the\nsame design with an unusual twist: the untrusted part is its own AI-written compiler, and only the\nsmall kernel's verdicts are trusted, a kernel whose type theory is machine-checked in Lean, though its\nauthor warns the kernel's code has drifted from that theory. Its critics found the limit the corpus names, in Kevin Buzzard's form:\nwhether the laws capture what the programmer actually meant is not something the kernel can check.\nFor Deliberus that is the same boundary: the kernel can refuse a malformed or unmarked machine write,\nand cannot tell a faithful split from a fluent wrong one. That residue is exactly what the sampling\nproof is for.\n\n**Added 2026-10-10.** The research on tidying machine-written proofs shows the same division inside\nmathematics, and five tests that no person has to judge are listed for any pass that rewrites or\nregroups:\n[alien-proofs-and-the-library.md](alien-proofs-and-the-library.md) § 4.5 (ledger AF2, unruled).\n\n---\n\n## 6. Level five: a resource that must not be used twice\n\n**Bend 2 is affine by default**: a value may be used at most once unless the program says otherwise.\nDeliberus has a resource with the same property. One piece of evidence can reach one conclusion along\nseveral paths (routed to three parts of one claim, it reaches the claim three times), and counting it\neach time manufactures strength from nothing. The corpus's evidence routing answers this with\n**fair-share discounting**: a fact routed to three children gives each a third, so its total is\nconserved, and the design deliberately refuses to round the shares because exact conservation is the\nwhole justification (`deliberus/evidence_routing.py`; built, tested, not adopted, since adopting it\nchanges every strength in the graph).\n\n**The founder corrected the design on 2026-08-15, and the correction is the part the formal\ntradition confirms.** Most apparent sharing dissolves once evidence is decomposed: *\"she published 47\npapers\"* is not one fact behind three children but a bundle, and each child draws on a different part\nof it. Fair shares stay right only for **genuine** sharing of an atomic finding, and what is missing\nis an evidence-decomposition pass ([decomposition-axes.md](decomposition-axes.md) § 2b).\n\n**Separation logic has exactly these two moves.** Its separating conjunction splits a resource into\n**disjoint** parts, each owned by one party, which is the evidence-decomposition pass; and its\n**fractional permissions** (Boyland 2003) give fractions summing to one only of a part that is\ngenuinely shared, which is fair-share discounting. The logic's rule of thumb matches the founder's\ncorrection: split first, and share fractions only of what cannot be split. By the kinship test\nproposed this morning (ledger S6) this is more than a metaphor: one problem (a resource reachable\nalong several paths must not be counted more than once) and one family of solutions (disjoint\nownership, then fractional sharing). **Verdict: Raised on mechanism.** It puts a mature formal\ntradition behind both the correction and the design, which matters only because adopting the design\nis an open founder call.\n\n---\n\n## 7. Level six: the vision\n\n**The company's bet is that general intelligence comes from symbolic search rather than, or beside,\nneural networks.** Search needs something to search against: examples to fit, laws to satisfy, a\nproof to check. The corpus reached the general form of this point about AlphaProof: a formal kernel\npays twice, by checking and by supplying free ground-truth reward, and deliberation has only the first\npayment, because what a Deliberus kernel certifies is validity of form, never truth of content\n([lean-deliberus-analogies.md](lean-deliberus-analogies.md), 2026 sharpening). Program search is the\nsame case: **in deliberation the specification is the thing in dispute.**\n\n**So whichever way the bet goes, the conclusion holds.** The harness conviction says the quality of\nmachine reasoning is a function of harness and grounding and is independent of architecture. If\nsymbolic search wins, it wins where a specification exists, and the two classes of error the\nconviction reserves for people (what the corpus silently omits, and the frame the graph grew inside)\nare exactly the places where no specification exists. The bet changes the tools on the machine side of\nthe line; it does not move the line.\n\n**One small resonance, recorded as resonance only.** HVM's slogan was that anything that can run in\nparallel will. Deliberus's version is addressability: a claim split into separable parts lets many\npeople work on different parts at once, with no one coordinating, while a bundled claim forces\neveryone to take a position on the whole. Separability is to deliberation roughly what independent\nrewrites are to a parallel runtime. Kept as a picture, not a claim, because the mechanisms differ\n(people do not reduce claims by local rules).\n\n---\n\n## 8. Verdicts\n\n| Idea from Bend's lineage | Verdict | Where it goes |\n|---|---|---|\n| Adopt either Bend as a language | **Rejected**: no speedup where the time goes; maximal maintenance risk | nowhere |\n| Unfold then fold (`bend` then `fold`) | Already present, under its classical name | nowhere |\n| Runtime sharing | Already done by hand (memoized strength walk) | nowhere |\n| Superposition for counterfactuals | Elegant, not needed at this size | nowhere |\n| Confluence as a property of graph construction | **Raised**; measured violation (59% one-sided pairs) | ledger T4; `TODO.md` |\n| Laws for deterministic code, samples for judgments | **Raised** | `TODO.md` (property tests) |\n| A deterministic invention law for splits | **Raised** | `TODO.md`, with the splitter's proof |\n| Small trusted kernel | Already the corpus's Lean analogy; Bend 2 confirms its limit | nowhere new |\n| Affine use ↔ evidence decomposition then fair shares | **Raised on mechanism** | supports an open founder call |\n| Symbolic-search AGI bet | Leaves the human-reserved line where it is | nowhere new |\n\n---\n\n## Cross-references\n\n[proving-a-pass-reliable.md](proving-a-pass-reliable.md) (the sampling half of § 5) ·\n[lean-deliberus-analogies.md](lean-deliberus-analogies.md) (the kernel analogy and the AlphaProof\nlimit) · [the-harness-conviction.md](the-harness-conviction.md) · [fractal-priors-for-success.md](fractal-priors-for-success.md)\n(maintenance as the class's killer) · [split-review-and-the-founders-intentions.md](split-review-and-the-founders-intentions.md)\n§ 4a (the overwrite) · [auto-connect-upgrade.md](auto-connect-upgrade.md) (the candidate generators) ·\n[major-transitions-heredity-and-evolvability.md](major-transitions-heredity-and-evolvability.md) § 8\n(the kinship test) · ledger rows R8, S6, T4 in [session26-open-rulings.md](session26-open-rulings.md).\n"}