I proved tennis scoring correct in Bend, then simulated the WTA Finals a million times

I was watching @poteto's video on how she shipped 2,500 PRs in one month (!) when I came across a reply she made to Victor Taelin's tweet about Bend. What is Bend you might ask? Those were my thoughts exactly. A few minutes of research soon procured the desired information. Bend (bend-lang.com) is a programming language whose pitch is the speed of C, the syntax of Python, and the scale of CUDA. The language's premise is that before writing any code, you write LAWS, then the AI writes the code plus PROOFS that it follows them. Thus, assuming the LAWS logic is correct, the AI model can write code, blocking mistakes via proofs, especially when introducing new features. As @GiulioRebuffo put it: // Detect dark theme var iframe = document.getElementById('tweet-2101337958821327199-359'); if (document.body.className.includes('dark-theme')) { iframe.src = "https://platform.twitter.com/embed/Tweet.html?id=2101337958821327199&theme=dark" } PROOFS A proof is a step by step argument that a law holds for every input. The way I see it, a law is a claim e.g It's going to rain tomorrow. A proof is my working out, my proof if you will, that it will actually rain tomorrow. It can't actually be proven if it will rain tomorrow but hopefully this helps get my point across. A good instance of its usefulness is in games. Below is a screen recorded video of a sample game from Bend's own website: Screen recordings of the interactive demo on bend-lang.com, by the Bend team (HigherOrderCO). Now knowing what Bend was, I was excited to try it out. My first instinct was to try it out as the backend in place of more traditional programming languages — a payroll app for instance. Wouldn't the LAWS prove especially useful as we're dealing with money which is quite delicate? Wrong. Turns out the hard part in creating a payroll isn't the math, it's talking to a money infrastructure API (Paystack in my instance), and Bend currently has no HTTPS or JSON support. 'Okay then' I thought, 'So ideally we'd want something mathematically heavy, something dealing with probabilities or a simulation of sorts'. After some brainstorming, I settled on an idea: A WTA simulator for the WTA Finals this November. What if I could select a seed of my choice, and then using recent Tennis data (I got all my data from Jeff Sackmann's 'Tennis Abstract' (data's licence: Tennis Abstract, CC BY-NC-SA 4.0) project, simulate what the odds of winning for a particular player is? Turns out this was the perfect use case for Bend. My idea, distilled down to its essence is this: I'm able to pick any 8 tennis players I'd like to match up against each other. Bend then simulates a million tournaments which comes down to about 15 matches per tournament (well, 2^20 which equals 1,048,576 times to be precise) based on recent data, and gives me the probability of each player winning the tournament. If you are interested, here are some more facts SPW refers to Serve Points Won. This is the share of points a player wins on her own serve. RPW refers to the return points won which are the share of points a player wins on her opponent's serve. To get player A's chance of winning a point on her serve against player B, the model takes player A's SPW, adds how often B fails to win return points i.e 100% - B's RPW, and then subtracts the tour average. This model, however, only covers the last 52 weeks on hard courts. Now playing a million matches sounded like some heavy computer work to me, but that's when a core feature of Bend became prominent to me called Parallelisation. This allows Bend to divide up your code and run it on individual cpu cores, and then tally it up. How is this possible you might ask? Well, two pieces can work at the same time if they don't depend on each other. This isn't the case with most programming languages: Variables are shared and changed by various parts. Bend however, has no hidden state; A function's result depends only on what you pass into it (a pure function; it's really similar to Haskell in this way). Thus, Bend's runtime is free to feed them to different cores If you want an even deeper dive, click me! To parallelise, you have to give your code that shape on purpose. Here's an example of some code in Bend doing just this: def Run.tally(+d: Nat, ..., +prefix: U32) -> Tally: match d: case 0n: Run.count(Run.single(fmt, ca, cb, seed, prefix)) case 1n+p: x y = Run.tally(p, ..., prefix * 2 + 0) Run.tally(p, ..., prefix * 2 + 1) Run.add(x, y) This looks a bit scary so let's break it down line by line: Line 1: def Run.tally(+d: Nat, ..., +prefix: U32) -> Tally: This declares a function (note the Python based def keyword). The function has arguments and let's start with +d . This denotes the depth of the expression. d being equal to 20 like it is in my code, is what gives 1,048,576. The + in front of the d marks an input that can be used more than once; Bend inputs are use-once by default. Marking it with the + means we can use the variable elsewhere. ... hides the match settings: the format, both players' chances and the random seed. prefix says which block of runs this call is responsible for (U32 types it as a 32-bit whole number). -> Tally (also typing) means it returns totals. Line 2: match d: Though similar, this isn't quite an if else type thing. match checks which shape d has: zero, or one-more-than-something. This is called pattern matching. Line 3 & 4: case 0n: Run.count(Run.single(fmt, ca, cb, seed, prefix)) That's 0n, the number zero (the n marks a Nat), not the letter O. At zero, stop splitting: play one match (Run.single, run number prefix) and turn its result into a tally (Run.count). Line 5, 6, & 7: case 1n+p: x y = Run.tally(p, ..., prefix * 2 + 0) Run.tally(p, ..., prefix * 2 + 1) Run.add(x, y) 1n+p matches any d of at least 1, and names one less than d as p. It makes two calls one level smaller, on blocks prefix*2 and prefix*2+1. Those are the two halves, and they run in parallel. x y = catches both results, and Run.add sums them. This allowed for fast simulation. On a 4-core cloud machine, a simulation of 1,048,576 best-of-three matches took about 21 s on 1 core and 5 s on all 4 (roughly a 4x speed-up). The full Finals run of 1,048,576 tournaments took 113 s on 4 cores. The next major concept, which I alluded to earlier, are LAWs. These are basically claims about every possible input, written in Bend. Let's go through one together to see how it works: Law 3: Deuce is never over law L3_deuce_is_not_over: for n: Nat {S.Game.winner(S.Game{3n+n, 3n+n}) == None{} : Maybe} 3n + n here means 3 plus n "What, Akintayo" I can hear you say. "How can that be?" Well confusingly enough, the n in 3n doesn't refer to a variable name but is instead a type suffix, typing 3 as a 'natural number' hence the name Nat. Anyways, 3n + n means 3 plus n. So, assuming n is equal to 0,1,2 and so on, we'd always have the same scoreline due to the S.Game{3n+n, 3n+n} line. For example, in the case when n is equal to 0, we'd have 3-3 and so on. This could theoretically go on forever, and it's why every match has a 1,000 point cap. ==None{} means that there's 'no winner'. So the law says that 3-3, 4-4, and every tie after that means no one has won the game yet. On this WTA project, I handled the conceptualisation of LAWS and the direction I wanted the project to go, while I used Claude Code for the coding. Basically, Claude would propose a rule or a spec change, I'd review it, and then it'd write the Bend code to align with this. Planted bug Caught by Game won with a 1-point lead L2 (the game rule) Point given to the wrong player L20 (each point goes to its winner) Points still counted after the game ended L5 (a won game is final) Set won 6-5 Set laws No tiebreak at 6-6 Set laws Serve order restarts every set Serve-order laws Match cap of 999 points instead of 1,000 L27 (the point cap) Half the runs counted twice L14 (every run counted once) The table above shows eight of the 24 bugs I planted across the game, set, match and simulation layers. Every one of them was caught. This I feel, is the real usefulness of Bend: the focus is placed on ensuring your Laws express what you want them to do, and then the code is written around them. For instance, when working on this app, the first 4 laws only said who won the game and ensured that a won game stays won. Going through them revealed a gap: if the wrong player is given points (e.g player A given the points of player B), the laws would still pass. And so a new law was added even before a line of code was written. This doesn't mean there can't be slip ups though, LAWS can only catch what they protect. If no law exists for a case, Bend is like any other programming language. For example, I had a filter which was meant to skip qualifying rounds (Q1 to Q3), however, it also skipped the quarter finals as it also began with 'Q'. There was no law for this and so it wasn't caught by Bend. Anyways, here's a screenshot of my end result of the running odds using a random seed: Title odds from one run of 1,048,576 simulated tournaments (random seed 18949729), using a sample field of eight players. Data: Tennis Abstract, CC BY-NC-SA 4.0. This was a really fun project and I'm still learning and finding Bend more and more intriguing as I go along. Excelsior! Akintayo.