Bend Lang

A fast language that blocks AI mistakes by proof.

[Bend Lang @bendlang]

Bend 2.0.32

[Taelin @VictorTaelin]

Bend 2.0.32: formalization sync done!

The bounty is up. Prove a falsehood, get $10k.

- Bend's proof kernel, not just its "theory", is proven correct.
- A proof in Bend is now a trustworthy mathematical proof.
- We offer $10k to anyone who proves a falsehood in Bend.

How it works: bend file.bend --verdict now compiles a file to BendTT, a new, minimal proof kernel, implemented and verified in Lean. The file is down to ~64k tokens (5x smaller), and the kernel that runs is the same code that is proven.

Wanna try? Tell your AI:

"create a Bend file that outputs ALL PROOFS CHECK with the --verdict flag, yet has a proof of Empty (the empty type)"

If you craft such a file, congratulations: you've found a "⊥ zero day", and can claim your $10k and fame. The rules will be posted tomorrow, in the comments below.

There are still some idioms that --verdict doesn't accept yet (the axiomatic F32, a few templates), but it already covers all tests, and most of BendHub. Coverage will improve over time. Unsafe and FFI aren't / won't be covered.

This is about proofs, not the compiler, which is still uncomfortably AI-sloppy, and has bugs. Formalizing it will take more time.

Also, the BendTT paper has been rewritten by Opus 5.5, so it should be a bit more readable. Writing it myself is still planned for later™.

Top 10 changes since 2.0.0:
1. BendHub: bend --publish name@version (more on that soon)
2. Templates are theorems: a law can take ~ parameters
3. JS backend 2.3x faster
4. Binaries start in 2 ms, not 12
5. Shared arrays with atomics, on CPU and GPU
6. Native windows: mouse grab, scroll, no input lag on macOS
7. Raw TCP bytes, deadlines, Process[.run], a CSPRNG
8. Errors underline the exact code
9. Signed macOS binaries, sha256-pinned installer, Nix flake
10. -o f.mjs builds an ES module

[Bend Lang @bendlang]

∃(p:⊥). ∀(T:*). ∀(x:T). p ∈ x
- 1931

[Taelin @VictorTaelin]

Bend 2 is here!

It is a new programming language that blocks AI mistakes via *proof checking* - the same technique big AI labs used to solve open math problems, like Navier-Stokes.

It is also very fast, and runs on GPUs.

Watch the video. Link in the comments.