Bend 2.0.39: Adequacy, Metal, and BendRT Milestones

Bend 2.0.39 strengthens proof evidence and fixes runtime behavior, while later development commits improve host memory reuse and JavaScript channels. This guide targets Bend 2.0.39. Development results through October 26, 2026 are labeled separately, not attributed to the release.

Release identity and evidence

The official release was published at 2026-10-23T21:40:41Z. Its tag is v2.0.39, at commit a3efe8a3801f423827424227172eed9802c5e6cb. Release PR #1840 records the shipped changes.

Our source manifest indexes captured GitHub JSON with SHA-256 digests and retrieval dates. Issue reports are distinguished from fixing PRs. These captures preserve upstream statements, not independent reproduction results.

Adequacy: what a checked equality establishes

PR #1627 adds BendTT adequacy. For a checked book, a closed, live proof term typed at an equality has convertible sides under the kernel’s reduction rules. Opaque definitions are interpreted at their models.

Consistency excludes a checked inhabitant of the empty type. Adequacy adds the connection between an accepted equality proof and conversion of its sides. Applying a law’s proof to closed values gives the closed instances covered by this claim.

The PR reports Lean 4.34.0 checks, a fresh leanchecker pass, and matching verdicts across 1,666 files. It also reports an unchanged kernel executable. The added theorem does not change the code run by Book.check or main.

This is not a proof that every generated native or GPU program implements an application’s requirements. Preserve model-to-implementation tests and review the specification itself. See our Bend introduction for the law-and-proof workflow.

Metal: removing a measured build regression

PR #1809 removes the Metal lane spill introduced in 2.0.38. Upstream isolated a device-program build increase from 0.257 s to 0.300 s, approximately 17%, on an M4 mini.

That is compilation overhead, not a 17% runtime speedup. The trade-off is explicit: a full lane again reports ERR_DEEP. Upstream identifies non-tail recursion under parallel evaluation reaching the Metal frame limit as a remaining failure case.

Separately, issue #1513 exposed a GPU closure missed in a later instance of the same datatype. PR #1542 revises ty_holds traversal to inspect value-indexed instances and handle growing families conservatively.

Its author reports CPU, Metal, and JS tests, but not CUDA validation. Do not read a cross-target compiler fix as evidence that every backend was independently exercised.

BendRT documentation now matches the runtime

Issue #1822 identified discrepancies between the paper and compiler. PR #1823 corrects the paper rather than changing the runtime.

The CPU corpus initially maps 2^33 bytes, or 8 GiB. It doubles in place toward 2^43 bytes, or 8 TiB, with residency growing as pages are touched. The initial reservation is not 8 TiB.

CUDA sizes the scheduling cube from L2 cache capacity. CPU and Metal retain the 128 by 128 configuration. The task-ring configuration must not be confused with the corpus layout, which remains 128 by 128 across targets.

JavaScript effects return tagged request objects carrying continuations. They do not unwind to the loop as thrown values.

PR #1813 corrects another cost model. Once a datatype is classified as hot, fields of every node receive counted-sharing treatment, including unshared nodes. Affine ownership does not imply that each unshared value avoids all reference-count traffic.

Ready IO yields without preempting pure code

PR #1723 limits each C and JavaScript scheduler turn to 64 ready effects. A parent repeatedly issuing ready IO can therefore yield to a runnable child.

This does not preempt pure computation or cancel losing computations. The author reports a deterministic progress test printing 73 on Bun and native C, not a throughput benchmark.

Process execution and native fault reporting

PR #1831 routes Process.run through one worker on Bun and Node. It addresses Node termination and children that leave stdin unread. The author reports 22 local cases across Bun, Node, interpreted Bend, and native C.

PR #1828 preserves native memory faults as fatal signals after a best-effort output flush. A parent can observe SIGBUS or SIGSEGV instead of an ordinary exit code of 1. This matters for crash supervision and diagnostics.

After 2.0.39: development commits through October 26

The following changes are not in v2.0.39. The latest covered merge is d30d7dddae6c40785ef03001455599baa31a8e2d. Pin a development commit explicitly before trying to reproduce these results.

Shared reuse of large host blocks

PR #1869 sends freed host blocks of at least 256 KiB directly to the shared bank. Other lanes can reuse them without waiting for another same-class free on the original lane.

For a repeated temporary-array workload on an Apple M5 Max, upstream reports peak RSS at 16 threads falling from 96.73 MiB to 66.92 MiB, approximately 31%. At one thread, both measurements were 65.59 MiB.

Smaller blocks keep their existing cache policy to avoid bank contention. Device frees keep their separate path. The author did not run CUDA or the full cluster gates locally.

Channel queues and timer lookup on JavaScript

PR #1859 replaces repeated front removal of parked waiters with a head-index queue. For 100,000 parked senders, upstream reports Node drain time falling from 3.35 s to 0.11 s on macOS arm64.

These are medians from 20 interleaved runs with Node 25.9. Bun’s corresponding result remained 0.09 s. This is a queue-specific result, not a general language speedup.

PR #1872 locates a woken timed waiter’s timer by binary search on JavaScript. Equal deadlines still require identity matching, and removing a timer still uses a linear array move.

For 40,000 timed senders per channel, an Apple M4 experiment reports median out-of-order drain time falling from 2,934 ms to 121 ms. The experiment used Bun and 15 interleaved runs per side. Native C is unchanged.

Retrying interrupted native writes

PR #1862 retries an interrupted native write without losing the offset accumulated by earlier short writes. Retrying the entire payload at application level could duplicate bytes already written.

The author reports a signal-driven pipe experiment where the original loop stopped after 65,536 bytes. The corrected loop wrote the full 1 MiB payload exactly once. Zero progress and permanent errors remain failures.

Benchmark methodology and adoption

This article targets Bend 2.0.39 but reports upstream experiments from individual PRs at their stated revisions. We did not rerun those experiments. Hardware, runtimes, sample counts, and limitations are attached to each result above.

The 16-workload benchmark explorer retains historical Apple M4 Max timings from September 17, 2026. Those figures are not fresh 2.0.39 measurements and are not combined with M4 mini or M5 Max results.

Use the released tag for reproducible adoption. Evaluate post-release fixes at immutable commits with your workload. Pair proof checking with requirement review, observable acceptance tests, and implementation correspondence checks using the verification framework matrix.