bend2-mega-skill
Made by JeffWrites, proves, parallelizes, builds and debugs Bend 2 (bendlang/bend) code or its compiler repo. Use when .bend files, LAWS.bend/PROOF.bend, parallel lets, GPU bangs, the bend CLI, or BendRT speed.
Works With
Quality and Utility come from canonical skill metadata. Community ratings appear separately as stars when subscriber reviews exist.
Subscribe to download
Public previews are available, but downloads, CLI sync, and premium content require an active subscription.
Sign In to Subscribe- Full skill content with deterministic versioning
- CLI sync + local search index
- Access to Jeffrey’s premium library
Save to your account
Saved skills live in your cloud list. Run jsm sync on each machine to pull them locally.
What's New with this Skill
1Updates, enhancements, and release notes for this skill.
New skill: bend2-mega-skill, laws an agent cannot quietly weaken
Bend 2 is dependently typed, affine and Python-shaped. The human writes LAWS.bend, the agent writes the code and PROOF.bend, and bend refuses a PROOF.bend beside a LAWS.bend it does not import. 35 references, 13 skeletons and 8 scripts, pinned to 2.0.13 and re-audited against 2.0.16, with the partial verdicts spelled out: "All terms check, with N unsafe annotation(s)" still exits 0.
- The human writes the law, the agent writes the proof, and the checker decides. bend refuses a PROOF.bend beside a LAWS.bend it does not import, so a proof cannot quietly discharge a weaker claim than the one that was agreed.
- Only "All terms check." is green. The partial verdict "with N unsafe annotation(s)" exits 0, and in 2.0.16 generated template instances count toward it without an explicit @unsafe. A smaller count after downgrading is not a stronger proof.
- Binders carry a quantity in {0, 1, ω}, spelled -x, x and +x. Writing the parallel let a b = f(p) g(p) needs that plus on the parameter; without it the second use fails with "consumed more than once".
- ERROR-TAXONOMY holds 84 error rows, and you get to yours without opening it: pipe bend's stderr into scripts/explain-error.sh and it prints the row plus the rule behind it.
- scripts/bench-speedup.sh interleaves the arms in both orders, takes medians, reports cv% per arm behind a refusal gate, can add an A/A null arm with --aa, and returns NOT_COMPARABLE instead of a speedup when stdout differs across modes.
- scripts/ledger-row.sh is weak on purpose: it does not verify laws, actual GPU dispatch, compiler identity or significance, and it never declares a WIN or a source revert.
- 21 inherited negative results ship pre-seeded in assets/ledgers/NEGATIVE-EVIDENCE.md, so the optimization loop starts by sweeping the graveyard rather than by rediscovering a dead lever.
- Pinned to 2.0.13 at 01e13b72 and re-audited against 2.0.16 at 981899d6. Two compiler defects ship with their reproductions: hyphenated imports emitting invalid JS identifiers, and F32.show decimal text differing between native C and JS.
- Thirteen skeleton files, checked under both audited revisions: LAWS/PROOF module, spec twin with fork tree and equivalence law, TCP server, headless App, CLI tool, a .bend module imported from JS under bun, and a custom effect in both C and JS.
- The walls are documented up front: Nat to 2^48-1, arity 255, refcount under 2^24, threads 128, ring 1024 at default CUBE_LOG=7, no CSE, no native Windows. bend2.dev is unofficial; the repo and bend guide are the authority.
A human states intents as laws in LAWS.bend. An agent writes the program and a PROOF.bend beside it. bend PROOF.bend is the gate, run after every edit, and only "All terms check." is green. "All terms check, with N unsafe annotation(s)" also exits 0, so a partial green reads as success to any script that inspects nothing but the exit code; the skill treats that as a state to report rather than a pass, and in 2.0.16 generated template instances count toward the unsafe total even without an explicit @unsafe. A smaller count after downgrading an annotation is not a stronger proof.