This hands-on tutorial with questions, try-outs and exercises is made because there isn't yet a beginners tutorial on the official and other Bend sites. The main target are Python developers, or other developers with a general programming experience.

It will be kept up-to-date with Bend's changes. Comments and corrections welcome!

https://github.com/Ivo-Balbaert/Bend-Tutorial

I've been writing a full Doom port in Bend 2 (2.0.36), and it's done enough to share.

Play: https://kbrianps.com/bendoom/ (runs on Freedoom; pick your own doom.wad or doom2.wad for the originals) Code: https://github.com/kbrianps/bendoom

What's in it

• Every episode of Doom and Doom II, every monster with the original states and AI, every weapon
• Menus, automap, intermission, finales (bunny scroller and cast call included)
• Saves in vanilla's .dsg layout: they load in Chocolate Doom and back
• PWADs with -file, including ZDoom's XNOD/ZNOD nodes (with a DEFLATE decoder written in Bend)
• Sound effects, OPL2/OPL3 music sample-exact with Chocolate Doom, and General MIDI through a SoundFont with modulators, reverb and chorus
• Mouse and keyboard, and a comfort mode for motion sickness

How it's checked test.sh downloads Freedoom and plays .lmp demos, comparing a per-tic trace (random index, player, and a hash of every mobj) with the one a patched Chocolate Doom prints. Frames are compared pixel for pixel and music sample for sample.

Bend notes About 18k hand-written lines. The game logic lives in one module because Bend refuses cyclic imports; per-frame data is in flat U32 arrays threaded linearly, since a tree lookup is far slower than an array read; and big flat records hit the "arity over 247" codegen limit. The browser build is the JS lane plus a small shell for canvas, keyboard, mouse and Web Audio.

Feedback welcome, especially from people who know the compiler better than I do.

I spent the last week building with Bend 2 on real projects, and came away pretty impressed. Quick thoughts:

1. Bend changes what the human needs to pay attention to.
   

Instead of reviewing every implementation detail, you can spend more time getting the intent and laws right, then let the coding agent figure out the implementation and proof. You still need to make sure the laws actually express what you want.

1. Coding agents make formal verification much more practical.
   

The annoying part used to be writing and maintaining the proofs. Now the agent can do that work. Basically: you don’t need deep math knowledge to start anymore; you can work through the problem in English and use the model to find the algebra/laws.

1. The proof is useful feedback for the coding agent, not just a safety certificate at the end.
   

This was probably the most interesting thing we actually observed. In one of our projects using Bend, the agent proposed roughly 20 laws. When we made it prove all of them, 4 of the original laws were actually false. The proving process found counterexamples, forced the edge cases to be stated correctly, and changed the implementation.

1. Bend being a real general-purpose programming language with formal verification built-in matters a lot.
   

Before Bend 2 existed, you might have your real program in Rust/TypeScript and separately model it in Lean/TLA+. Then you have to trust that the thing you proved still matches the real program. Bend lets the code you execute also be the thing whose laws you prove. No more worrying about the 'model of your code' drifting from the real code.

1. You probably shouldn’t formally prove everything.
   

This was an important conclusion for us. Use it where correctness really matters, where the logic has a clear mathematical shape, where agents keep tripping up, or where there's a core that will evolve a lot. Proving every trivial piece of an app can be overkill and costs more tokens/time.

1. You don’t have to rewrite your whole app in Bend to use it.
   

It's easy to get started. We took one correctness-critical part of one of our existing TypeScript projects, rewrote just that slice in Bend, compiled it to JavaScript, and left the rest of the application alone. It is now 100% bug-free (actually proven!) and 4x faster.

I recorded the workflow step by step here if anyone is curious: YouTube

Would also be curious how other people here are thinking about Bend / applying Bend in their projects.

I am writing a linear programming solver (first-order) and am trying to make it fast. I am only giving Astra the standard instructions from 5.2 on bend-lang.com.

I am noticing that Astra looks a lot at the generated C code, tweaks the Bend code and iterates until the C code becomes what it wants. At this point, it feels a little like C programming with extra steps. Any suggestions on how to avoid this?

(I don't mean to come off as negative at all, this is likely just a skill issue on my end.)

Write a pure function in Bend, prove it correct for every input, and import it in TypeScript with full types.

bend-emit compiles a Bend file into an ordinary typed ES module.

https://github.com/nohzafk/bend-emit

Title,

Basically for me the github repo of Bend2 is a 404

https://github.com/bendlang/bend/

I didn't like seeing the code without colors, so I vibe-coded an extension for Zed and its tree-sitter

https://github.com/FabianVegaA/tree-sitter-bend

https://github.com/FabianVegaA/zed_bend

The hub has no names, versions, or search (`import 0x…/file.bend`), so GitHub is the catalog for now.

I put together a list for current Bend (`bendlang/bend`, 2.0.x): https://github.com/777genius/awesome-bend

Already on it: official compiler/guide/demos, bend-batteries (JSON), bolt (LSP), tree-sitter, nix flakes, from-zero, a few community demos.

PRs welcome if you have something running.

Hi, my agent gets the following error all the time:

 /home/petter/.bend/bin/bend: 59: cannot create /home/petter/.bend/last: Read-only file system

Is it possible to fix/disable writing somehow? Is it telemetry?

I'm just wondering if the fruit fly brain can be formalized to support things like "proof that a fly can learn basic arithmetic".

Is there any way i could programm my FPGA with bend? Could be much easier than Verilog.

Let's make this question viral and overperform the famous "will it blend?" :-)

Bend deserves some hype!

i am really excited about Bend and immediately rushed to try exactly this test to see how Bend will manage exponentially growing number of calls.

Why this important case is commented out in examples?

u/SrPeixinho is it on your radar to address and optimize cases like recursive Fibonacci?

BTW, thank you a lot for your great work!

P.S. wow, i am the very first member! 🤓