I rewrote a vehicle routing algorithm in Bend and measured it against Java

The problem, in one paragraph

A distributor serves a few dozen cities from a single depot. Each truck has limited capacity, each driver has a limited working day, and when a route doesn’t fit in one day the truck stays overnight at an approved hotel and continues the next day. The algorithm sends out an “ant” that builds an entire plan by making probabilistic decisions at each stop, and repeats this 6 million times (15,000 iterations with 400 ants each), keeping the best plan.

For the benchmark, what matters is the shape of the workload: the ants in one iteration are independent of each other. None of them writes to anything another one reads. It’s textbook parallelism.

First contact: Bend is not Java with different syntax

The first version didn’t come close to compiling. Bend has a set of restrictions that seem arbitrary at first, and after a while you realize almost all of them exist to guarantee that the program can be cut into parallel pieces without complicated analysis.

There is no if. You pattern match on a parameter:

def pickf(c: Bool, a: F32, b: F32) -> F32:
  match c:
    case True{}:
      a
    case False{}:
      b

And match only works on parameters or pattern variables, never on a value you just computed. That pushes the code toward continuation-passing: instead of computing a value and taking it apart, you pass it to a function that receives it as a parameter. Half of the port turned into helper functions with names like city_stats and city_pick because of this.

There is no mutual recursion. The original Java loop had two phases that called each other: pick the next stop and apply the move. In Bend it became a single loop, with a choosing flag saying which phase it’s in:

def ant(fuel: Nat, go: Bool, choosing: Bool, st: Stats, pk: Pick, ...) -> Sol:
  match fuel go choosing st pk:
    case 1n+f True{} True{} Stats{...} _:
      # phase 1: look at the options and draw the next stop
    case 1n+f True{} False{} _ Pick{...}:
      # phase 2: move, and compute the options for the next step
    case 1n+_ False{} _ _ _:
      # done
    case _ _ _ _ _:
      # out of fuel

The guide is explicit about why: “Termination is mandatory and mutual recursion is not allowed. Both restrictions keep Bend’s proofs sound, as a function that never returns could otherwise prove anything.” There is a termination checker that wants to prove your recursion decreases, reading the arguments from left to right. A loop that ends on a logical condition, like the ant’s, doesn’t decrease anything, so you either mark the function @unsafe or pass in fuel: a natural number that shrinks on every call and caps the recursion. The ant’s fuel comes from simple reasoning: at most one visit, one overnight stay and one return to the depot per city, two calls each. The checker is literal about order. One of the functions failed only because the shrinking argument was the second one, and the first one changed before it. Swapping the parameters fixed it.

Values are affine. By default you use each value once, and to reuse one you mark it with +, which makes the value shared through reference counting. That + goes on the parameter, not the type (+tab: Tab), and it took a good handful of syntax errors to get it right.

None of these restrictions come free for the person writing the code. But they all push in the same direction: immutable structure, no surprise aliasing. That’s the entry fee for automatic parallelism.

What changes in your head when you come from Java

The difference isn’t in the syntax, and that was the part that caught me off guard. In Java the ant is a stateful class: an object holding the current truck, the load, the minutes left in the day, the list of cities already served, the random number generator. Each step is a method that modifies those fields. You read the code from top to bottom and the state changes along with it.

final class Ant {
    final boolean[] delivered = new boolean[n];
    int left = c;
    int cur = 0, load = 0, trucks = 0;
    double j1 = journey, j2 = journey;
    ...
}

In Bend there are no fields to modify. Everything the ant knows becomes a parameter, and the parameter gets passed along on every call. The same loop has eighteen arguments, because every little piece of state that lived in a field in Java now travels explicitly: the current position, the load, the two days of working hours, the accumulated distance, the trucks, the served cities as a bitmask, the random seed, the route built so far. The whole file has seventy-nine definitions, almost all of them small, because match only works on parameters and any computed value has to be passed to another function to be opened.

This has a side effect that hurts when you want to change things. In Java, adding a piece of information to the algorithm means adding a field. When I wanted the ant to also read the pheromone tree, I had to thread a new argument through six chained functions, each with an already long parameter list, and fix every call. It isn’t hard, it’s tedious, and it’s the kind of thing that makes you think twice before trying out an idea.

The upside is that state stays where you can see it. Without mutable fields there’s no “someone changed this somewhere else”, and that’s what let me run the same function on eleven cores without thinking about synchronization. What is cheap freedom in Java (aliases everywhere, writes anywhere) is an explicit decision in Bend: reusing a value requires marking it with +, and the compiler sends you the bill in reference counting.

The compiler, by the way, is a strict teacher of few words. The messages I saw most were three: consumed more than once, when a value is used twice without +; expected a decreasing self-call, when the recursion doesn’t convince the checker; and the rejection of a nested match, which forces you to create yet another definition just to open a record. Each one is a small rule, and together they push you toward a very particular style. At first it feels like the language is getting in the way. After a while I realized I was writing code that couldn’t have a race condition, because the wrong way to write it doesn’t even compile.

The difficulty I didn’t see coming was debugging. Pure code in Bend doesn’t print, because effects live in the IO block, so you can’t scatter a print in the middle of the ant loop and see what happens. What’s left is returning values and measuring the whole program. That’s exactly how I found out where the pheromone time was going: compiling three versions of the program and comparing the clock. It works, and it’s much slower to do than a System.out.println inside the loop.

If I had to sum up the difference in one sentence: in Java I describe what the machine should do with memory, and in Bend I describe how the data is transformed. The second way costs more to write, especially when the algorithm is stateful by nature, and it gives back a program the machine can parallelize on its own. The trade isn’t always worth it. For the ants, which are independent by definition, it was.

The parallelism model

The central construct is a two-legged let:

a b = colony(p, rows, lo, mid) colony(p, rows, mid, hi)
better(a, b)

The two calls can run on different cores. There’s no thread annotation, no pool, no join. You write the fork tree and the runtime distributes it.

The detail that changes everything in practice is in the guide: “Bend’s current scheduler is a contention-free, binary fork-join machine: every task is handed to a core exactly once and never moved afterwards. That makes it fast and GPU-friendly, but you must keep the workload balanced.” No task migration means no contention, and the same model works for the GPU. On the other hand, if you spawn 4 fat tasks and have 11 cores, 7 sit idle until the end, and if one task is much bigger than the others, the total time is its time.

The design rule that follows is wide and shallow, with balanced leaves. In the ACO this came naturally, because the ants are all alike: the solution is a balanced binary tree of forks over the range of ants, and each leaf runs a handful of them in sequence.

def colony(+depth: Nat, +rows: TabW, +it: U32, +lo: U32, +hi: U32) -> Sol:
  match depth:
    case 0n:
      ants(U32.is_lt(lo, hi), rows, it, lo, (hi - lo : U32), Sol{INF(), 0, []})
    case 1n+p:
      +mid = (lo + ((hi - lo : U32) >> 1n : U32) : U32)
      a b = colony(p, rows, it, lo, mid) colony(p, rows, it, mid, hi)
      better(a, b)

Where this hurt was in another algorithm, written later: an iterative local search (ALNS). There the work is naturally sequential and long, a chain of thousands of successive improvements. Running 16 chains on 11 cores gave a 1.8× speedup, not 11×. The way out was to rewrite the search in rounds: each round forks 256 short chains from the best plan so far and keeps the best one. It became more parallelizable and, in the end, faster in quality per second. But that’s a change of algorithm, not of code. The language forces you to rethink the shape of the problem.

The numbers

Everything ran on a MacBook Pro M3 Pro, compared against a Java port of the same algorithm using arrays and ForkJoinPool. Same instance, same random number generator, same candidate order, so you can compare step by step, not just the final result.

The persistent pheromone row is the one I repeated the most, because it was the one that surprised me. In scenario 1, with the machine idle, Java solves it in 18.3 s and Bend in 111.7 s, two consecutive runs with the same number. Running all five scenarios, the average is 17.2 s versus 108.4 s. Both plans use seven trucks and are within 0.8% of each other.

Solution quality was the same within ~2% in every case, which is the natural run-to-run variation of these algorithms. This is not a trade of precision for speed.

On scaling across cores, with 200 × 400 ants:

For me this is the most interesting result of the benchmark. Bend loses on the constant, not on parallelism: it uses the cores slightly better than my Java code with ForkJoinPool, it just starts from a higher point.

Why the ratio varies so much: 2.4× or 8×?

The number changes from program to program, and the pattern is clear. The ratio gets worse the more the program allocates.

The original ACO is an arithmetic loop over an immutable table built once. It barely creates any new structure, and it stays at 2.4×.

The ALNS creates new lists all the time, because every candidate route is a new list, and every distance between two cities is a walk down a tree instead of a dist[i][j]. I measured the operation in isolation: evaluating a route costs ~1.1 µs in Bend versus ~0.1 µs in Java. That’s where the 8× comes from.

It’s worth saying that a lot of this is negotiable with effort. The first working version ran in 12.6 s single-threaded; after reorganizing the instance as a balanced tree traversed once per step, and replacing pow with multiplications in the hot loop, the same workload dropped to 2.7 s. The shape of the data matters much more in Bend than in Java, because without indexed access to contiguous memory, the hardware can’t save a badly chosen structure.

The experiment that taught me to think in Bend

The pheromone case turned into the most instructive part of the work, and it’s worth telling in detail because I got it wrong twice before I understood it.

The pheromone version needs a matrix that every ant reads and that gets updated at the end of each iteration. In Java that’s a double[][] and you write to it. In Bend, the implementation builds a pheromone tree, evaporates the whole thing every iteration, deposits on the edges of the best route and builds the weight table the ants read. My first guess was that this was pure waste, and that the language needed an array with in-place writes.

I checked the documentation before publishing, and the array already exists: “An Array<T> is a Type, so it has exactly one owner at all times. That is what lets a[5] <- 42 overwrite the slot and hand back the same array, with no copy.” It’s the mechanism I was going to ask for, already implemented. But the shader guide has the restriction that settles the matter: “An Array has one owner, so it cannot go down a fork tree: build lists.” Any structure read by millions of tasks in parallel really has to be a shared tree. Arrays don’t apply here.

So I went to measure where the time actually went, with 500 iterations of 400 ants on 11 threads:

Evaporating and depositing costs 28 ms over 500 iterations, or 0.06 ms per iteration. That’s noise. The 3.6 ms per iteration I thought was pheromone maintenance is actually building the weight table the ants read.

The obvious fix would be to build no table at all: let the ants read the instance tree and the pheromone tree side by side, step by step. I rewrote it that way, and the result was the opposite of what I expected:

Both versions find exactly the same plan, and single-threaded they’re practically tied. On 11 threads the second one stalls. The reason is in the guide, in a sentence I had read without understanding: “a + value read by every lane costs an atomic per read”. Every read of a shared structure costs an atomic reference-count operation, so reading two trees per step doubles that traffic and eats the parallelism.

The lesson I take from this: in Bend, rebuilding data can be cheaper than sharing one more structure. It’s the opposite of the instinct I brought from Java, where allocation is expensive and reading a shared structure is free.

The GPU: excellent or useless, depending on the program

In Bend, sending a call to the GPU means changing f(x) to f!(x). It compiles a Metal kernel along with the binary, and it’s one of the most impressive things to use.

The result depends entirely on the shape of the work. The ACO on the GPU ran in 8.6 s versus 33 s on the CPU, and versus Java’s 13.7 s on 11 threads: the ants all run the same short loop over the same table, which is the ideal case. The ALNS on the GPU, on the other hand, was 16 to 28× slower than Bend itself on the CPU, because each chain takes a different branch at every step, allocates all the time and reads a shared table.

The guide warns you about this before you try: “The GPU shines on uniform numeric work like mandelbrot or nbody; divergent work like n-queens stays faster on the CPU.” The plans generated on the GPU and the CPU were identical, so the divergence is only in performance. The lesson is the same as with CUDA, with an ease of use nothing else comes close to.

Proofs: the part of the language I didn’t expect to use

The first line of the Bend guide says it combines “Lean-like formal proofs with C-like speeds and CUDA-like parallelism”. I had read that as marketing and only looked into it at the end of the work, when I already had three implementations of the same algorithm and wanted to know whether they agreed by chance or by construction.

The mechanism is straightforward. You write a law, which is a statement with quantifiers and an equality:

law truck_capacity:
  for k: Nat
  for it: U32
  for a: U32
  {Rules.capacity(plan(k, it, a), 0) == True{} : Bool}

And you prove that law with a definition of the same name in another file. Running the proofs file checks everything and fails while any law is still open, with a blunt message: Error: 11 TODOs found. The code is incomplete, and not a valid proof yet. One file says what must hold, the other says why, and the compiler won’t let you mix the two up.

The simplest proof is {==}, which is reflexivity: the checker evaluates both sides and sees the same value. That closes any law that is a closed term. The laws about the model’s parameters went through that way, and so did three facts about the instance, by case analysis over the 81 locations: distance doesn’t depend on direction, staying put costs zero, and each city’s demand fits in one truck.

What didn’t go through were the interesting laws. Saying that every ant respects capacity requires induction over the ant loop, showing that each step preserves the invariant. Bend can express that proof, but writing it is a project the size of the algorithm itself, and I didn’t write it. I tried a shortcut that seemed clever: state the law for one specific ant, which becomes a closed term the checker could just evaluate. It has to normalize an entire ant over 58 cities and hadn’t finished after 14 minutes. Proof by evaluation reaches parameters and facts about the instance, not a run of the solver.

Even without the proofs, the exercise paid off, and for a reason that isn’t what the marketing sells. To state the rules I had to write them as functions that read the raw instance and take a finished plan, without trusting anything the solver had precomputed. That gave me an independent judge, and an independent judge was exactly what I was missing to compare implementations. Since the laws are executable, they work as tests: I ran the checkers on 400 ants, with the initial pheromone and again after twenty iterations, and the rules the program guarantees pass on all of them. The ones it doesn’t guarantee come out false, which is precisely what I wanted the tool to tell me.

My conclusion on this part is less enthusiastic than the slogan and more useful than it. Stating is cheap and immediate; proving is expensive and is still human work. The real gain of having the proof system in the same language as the program is that the specification stops being a comment and becomes code the compiler checks, runs and holds you to. I’d take that to any project, whether or not I ever close the proof.

What I’d still ask of the language

After checking my list against the documentation, three requests were left.

Load balancing in the scheduler is the first. The current behavior is deliberate and consistent, and the guide itself uses the word “current”, which suggests the authors see it as a stage. Today balancing is the job of whoever writes the code, and that’s what turned “run 16 chains” into “rewrite the search in rounds”.

The second is power with a constant exponent. F32.pow exists as a primitive, but I found nothing about specializing a literal exponent, and in practice it was a fifth of the runtime until it became hand-written multiplication.

The third is a profiler. There’s nothing in the guide, and no CLI flag besides --threads and --gpu. Today you find out where the time went by measuring variations of the whole program, which is exactly what I had to do to find the cost of the weight table. Knowing how many interactions each definition consumed would change the optimization loop.

One observation worth more than the list: Bend’s documentation is dense and answers much more than it seems to on a first read. Two of my wrong conclusions were corrected there, in one sentence each.

Is this problem a good fit for Bend?

Half of it is, and it’s worth separating the two halves carefully.

Candidate generation is an almost ideal case. Millions of short, independent simulations, all doing the same kind of work over a table nobody writes to. It’s the shape where automatic parallelism shines, and it’s where a single ! put the GPU 1.6× ahead of Java on 11 threads, without writing a line of kernel code. If your problem looks like this, such as Monte Carlo, parameter sweeps or population evaluation in a genetic algorithm, Bend delivers what it promises.

Refining a solution is a bad case. Local search is a long, sequential chain of small modifications, with branching at every step and random access to structures. It doesn’t parallelize on its own, it doesn’t like the GPU, and it’s where the tension between “shared by many tasks” and “fast indexed access” shows up in full, because the two don’t go together today. You can reformulate it in short, wide rounds, as I did, but then you’re changing the algorithm to fit the machine, and a different algorithm may simply be worse.

The practical conclusion is that granularity has to be chosen with the scheduler in mind, not the problem. In Java I’d decide it thinking about cache and contention. In Bend I decide it thinking about how many similar leaves I can generate, and how many shared structures each leaf needs to read.

Final analysis

After a few weeks of this, here’s my take.

What Bend really delivers is parallelism without you writing any parallelism. There was no mutex, no race condition, no deadlock to debug. The program that runs on 1 thread is exactly the one that runs on 11, and the one that runs on the GPU differs by one character. That’s the part of the work that usually eats the most time and produces the most subtle bugs.

What it charges is a factor of 2 to 8 against well-written Java, and almost none of that comes from the scheduler. It comes from data representation, and part of it comes from modeling decisions that only become obvious after measuring, like the weight table one.

I got something I didn’t expect. Rewriting the algorithm without any mutable state made explicit several decisions that were implicit in the Java version, and once the two versions started giving equivalent answers I had much more confidence in what the algorithm actually did. Rewriting in a language with stricter rules is an expensive but effective way to review your own code.

In the end, Bend today is not the choice for squeezing out the last cycle; Java, Rust or C still win that. It’s the choice when the bottleneck is your time, and the question is how many cores, or which GPU, you can use without turning your code into a synchronization minefield.