Bend 2 joins proof obligations to parallel programs
Bend 2 asks you to describe important behavior as laws, then supply definitions that prove those laws. The same pure language compiles to C, CUDA, Metal, and JavaScript. A ! call marks work for parallel execution, while the type system tracks affine values that cannot be copied freely. This is an unusual combination: proof checking and parallel execution live in one compiler instead of separate application and verification tools.
The promise needs a tight boundary. A proof establishes the law you wrote, under the language's rules. It cannot tell you that the law captures every product requirement or that foreign C and JavaScript effects behave correctly. The guide says @unsafe recursion falls outside the proof guarantees, and host effects never enter the proof system. Bend 2 can make a precise invariant enforceable, but somebody still has to choose the invariant and review the seams around it.
Bend 2 laws demand explicit proof work
Bend 2 pairs each law with a definition of the same name, and bend PROOF.bend checks whether every claim has been filled. There are no proof tactics or proof search. Case analysis, induction, equality rewrites, and explicit witnesses are the working tools. That makes the mechanism easier to inspect, but it also moves effort into annotations and proof definitions that many application teams have never maintained.
The language makes other deliberate trades. Almost nothing is inferred, recursion must terminate unless marked unsafe, and computed matches have to be split manually. Values are affine by default, so closures, arrays, and IO handles cannot simply be shared. The README also lists only Nat, U32, and F32 numbers. F32 is axiomatic, which means floating-point properties cannot be proven inside the system. These limits may be acceptable for a proof experiment and painful in an ordinary service.
What happened when we ran it
Our sandbox installed Bend's package workspace in 8 seconds. Bun added 4 packages and used 7 MB on disk. The checkout was commit a495242, with 1,774 files, about 22,735 source lines, and 74.7 MB of repository data. The measurement setup was an unprivileged Debian container with 3 CPUs, 8 GB of RAM, no secrets, and the project located under bend2/pack/.
No build script or build target existed in that package, so the lab skipped the build step. The package also exposed no test script or test target, so tests were skipped. Those are not passing results. The repository does contain a tests directory, but our supplied commands had no package target that exercised it. We measured repository setup, not Bend program speed, proof-checking speed, CPU scaling, or GPU throughput.
Four packages hide a larger native toolchain
The 4-package install makes the JavaScript compiler workspace cheap to fetch, yet native use reaches beyond Bun. The guide requires clang 14 or newer for a binary. Programs using ! need clang 19+, Metal, or CUDA 12, and the generated GPU companion file must stay beside the binary. Linux window and audio effects require X11 and ALSA headers. There is no Dockerfile to turn those requirements into a ready image.
Bend's one-line installer is still the quickest evaluation route, with Homebrew and Nix alternatives documented in the v2.0.25 release. Platform reach is narrower than the four targets suggest. Native Windows is absent, though WSL works. JavaScript runs on one core and has no graphics or audio. A program can use one GPU, one event loop, and one generated C file, with no separate or incremental compilation. That is a research-friendly toolchain, not a drop-in service runtime.
GPU work must divide cleanly
Bend 2 does not make every function faster when you add !. The README says parallelism requires balanced calls and labels shared arrays with atomics as experimental and unsafe. Open issue 942 reports that a sequential workload sent to the GPU under Bend 2.0.23 held a Metal command buffer until the macOS watchdog killed WindowServer. The report is specific to that workload and machine, but the failure is serious enough to reproduce before trusting GPU jobs on a workstation.
The checker has young-compiler failures too. Open issue 973 demonstrates a four-line invalid program that kept one CPU core busy until the reporter interrupted it after 20 seconds. The report used Bend 2.0.25 at the same a495242 commit our lab received. This does not show that checked Bend programs can violate their laws. It does show that untrusted source can trap the checker before a useful diagnostic appears, which matters if an automated agent feeds code into it.
Release 2.0.25 is active, while audit work remains
Bend 2.0.25 was published on September 21, 2026, and the repository was pushed again that day. GitHub listed 44 open issues and pull requests, with reports and patches updated through September 22. The release fixed compiler edge cases, macOS FIFO handling, and generated C name collisions. That combination points to active maintenance rather than a dormant experiment, though the combined GitHub count should not be read as 44 confirmed bugs.
Activity cannot substitute for maturity. The README says the compiler is 99% AI-written, has not been fully audited, and differs from the Lean formalization. It also lists no test framework, debugger, profiler, or REPL, while the language server only formats code. Bend earns a trial when a small number of formal laws could prevent an expensive class of mistake. Until those gaps close, keep the trial isolated and make the proof boundary explicit.