Bend – a language that blocks AI mistakes via proof and runs on GPUs
A new programming language called Bend aims to let developers specify formal “laws” that AI‑generated code must satisfy, using an affine dependent type system and GPU‑accelerated runtime to check proofs quickly. Commenters are intrigued by the idea of constraining LLMs with machine‑checked invariants, but raise practical concerns: writing complete, correct laws may be as hard as writing the program, underspecified laws can be gamed, and the current ecosystem (stdlib, ergonomics, tooling) is still immature. Trust issues also surface around the project’s heavy use of AI in its own code and documentation, earlier deletion of git history, and bold performance and correctness claims relative to mature proof assistants like Lean or Agda.
Project goals & positioning
- Bend is presented as a language with an affine dependent type theory, aimed at proving “laws” about programs and compiling to efficient CPU/GPU code.
- Core idea: humans/agents write a small LAWS.bend spec; AI (or humans) write the rest; compiler checks that all code satisfies the laws.
- Marketed explicitly for the “post-AGI” world and for LLM-based coding agents.
Repo history, trust & AI-generated code
- Large concern about the GitHub repo being squashed to a single commit, erasing history, forks, and reproducibility; seen as a trust issue, especially given big claims.
- History was later restored after pushback; some argue this was overblown, others see it as crucial for auditability and benchmarks.
- Significant parts of the compiler/docs were generated or helped by LLMs; some see this as normal, others as “AI slop” and a red flag when combined with grand claims.
Type system, proofs & “laws”
- Bend uses linear/affine types and quantity-indexed universes, prohibiting runtime closure cloning to ensure termination and good GPU behavior.
- Laws are essentially invariants/proofs checked at compile-time; tests are explicitly contrasted as not providing the same guarantees.
- Multiple commenters note the classic problem: specifying correct, non-vacuous laws for large systems is at least as hard as writing the code.
- Risk of “negative space programming”: AI satisfies laws by changing the problem (e.g., game movement rules, world size) rather than reflecting user intent.
Performance, GPU story & comparisons
- Claims of order-of-magnitude faster proof checking vs Lean/Agda/Isabelle are met with skepticism:
- Bend avoids unification, tactics, and inference, so comparisons to full-featured elaborators are seen as misleading.
- GPU use is currently for runtime parallelism; compile-time proof checking on GPU is “not yet.”
- Some are interested in the interaction-net/HVM lineage; others note Bend 2 is architecturally different from earlier work.
Language design, ergonomics & docs
- Docs (GUIDE) are praised for ambition but criticized as confusing:
- Questions about erased arguments, Kind parameters, array syntax, and surprising types like
Array<T> & U32. - Arrays/linearity lead to unintuitive APIs (reads returning
(array, value)), acknowledged as likely needing redesign.
- Questions about erased arguments, Kind parameters, array syntax, and surprising types like
- Lack of tactics and inference makes proofs verbose; author’s stance is that verbosity is acceptable if AI writes proofs.
Adoption, ecosystem & alternatives
- Concerns about:
- Tiny stdlib, lack of math libraries, and difficulty porting large existing proofs from systems like Cubical Agda.
- Missing or nascent tooling (changelogs, releases, integration with existing languages).
- Some are enthusiastic and experimenting (e.g., porting small apps, meeting schedulers); others prefer existing tools like Lean, Coq, Dafny, Verus, or proof-like contracts in mainstream languages.
- Several note this is promising early-stage research/engineering, but current marketing overstates maturity and scope.