Latest / Superlinear / How to Build and Verify Agent-Written Code with Bend 2

Transcript

How to Build and Verify Agent-Written Code with Bend 2 · Superlinear

• 0:00
  Christine: Bend2. If you use coding agents, Bend is interesting because it could turn more of please get this right into something the machine can actually check. So Bend is a new programming language with formal verification built in.
• 0:17
  Christine: So you can write normal software and also prove that certain properties of that software are true. So what is formal verification?
• 0:27
  Christine: What is actually different about Bend and how does it change how we should build with coding agents?
• 0:33
  Christine: By the end of this episode of the Superlinear podcast, you'll understand how Bend works, where it fits next to things like types and tests, and how you can try it on one part of your own project.
• 0:47
  Christine: So, Brandon, what makes you so excited about Bend?
• 0:51
  Brandon: Look, I'm so excited about Bend because the best way to build with coding agents is to really understand the thing you wanna build, whatever it is, if you're starting from scratch, if you're adding a feature, share that information with the agents and put as many guardrails as you can that the agents can autonomously use to make sure that the thing that it's writing is correct before it comes back to you.
• 1:22
  Brandon: This is especially important these days because the models are getting smarter, the agent harnesses are getting better, and you can do more and more off in the background and what we wanna do is set ourselves up so that the thing that comes back after six hours, a day, three days is already correct so that we don't have to go back and forth with the agent to try and fix things up.
• 1:51
  Brandon: And so this is how, like, we should all already be trying to work, right?
• 1:57
  Brandon: And what Bend does is it's the first programming language ever that still is a general-purpose language that you can build real stuff in.
• 2:09
  Brandon: You can build stuff fast, you can build stuff for the web that also includes the ability on top of a strong type system to formally verify the correctness of the implementation.
• 2:24
  Brandon: And this is just like so crazy, so cool.
• 2:27
  Brandon: Anyway, I'm really excited to talk about it.
• 2:31
  Christine: But was there already other formal verification tools or languages that you were already using for agents? What changed when Bend2 came out?
• 2:43
  Brandon: Yeah, so there's a fair number of formal verification tools that have been around for a while and typically have been maybe too difficult for humans to justify using in their everyday projects. And with agents, people have started to use them more. So tools like TLA+ which help you verify the correctness of your distributed applications, concurrency related issues, TLA+ can help you with tools like Lean have been used to formally verify a lot of mathematics proofs. And I've experimented and some people have experimented with proven correctness of software written in another language using Lean.
• 3:30
  Brandon: Actually, sorry, I need to show a tweet.
• 3:35
  Brandon: Who used these two tools recently Boris.
• 3:39
  Brandon: OK, let me pull up the tweet. Give me a sec
• 3:42
  Christine: Boris from Anthropic.
• 3:45
  Brandon: Yes, Boris from Anthropic.
• 3:50
  Brandon: So Boris in the Opus 5.5 announcement said that he used Opus 5.5 to formally verify the Claude Agent SDK using Lean and then he also said TLA+ works well and that he combines Lean and TLA+ to look for issues around data flow, concurrency, and state management and then he goes on to say he doesn't know either language well but Claude is excellent at both and then in the thread he later says that using these tools actually diagnose and help him fix bugs in the Agent SDK, which is really cool.
• 4:27
  Christine: So cool. Boris also using formal verification.
• 4:31
  Brandon: Yeah. So formal verification is something that, like, is totally worth taking a look at now because agents can help deal with the hard stuff.
• 4:40
  Brandon: But what happens when you try and use these tools like Lean and TLA+ beyond a sort of focused bug-finding mission, but if you actually wanna use these tools to maintain the correctness of your application over time and to help your agents in all the work that they do write correct code, is that these tools are different programming languages.
• 5:04
  Brandon: And so you basically have to re-implement your code over and over again. So you have your main implementation in whatever, TypeScript or Rust or something like that.
• 5:13
  Brandon: And then you write a version of the application in TLA+ a version of the application in Lean.
• 5:22
  Brandon: And it's really hard to keep them in sync, And some people have tried a bunch of things like Doodlestein has a bunch of skills that help him keep his Lean code in sync with his Rust code for some of his projects.
• 5:38
  Brandon: And I've played with that a little bit.
• 5:40
  Brandon: But it's messy and Lean is really good at proving the correctness of math like and a lot of abstract math.
• 5:52
  Brandon: And it's a little bit less helpful for proving the correctness of programs.
• 5:57
  Brandon: But Bend is good at it.
• 6:00
  Christine: So with the previous formal verification methods, the thing that you were actually proving is a separate model or specification of your real implementation. So the risk when you do that is that this representation can differ so I guess it means that the practical risk is that your implementation can differ from the model that you proved, or it can drift away from it later.
• 6:33
  Christine: Is that right?
• 6:37
  Brandon: Exactly.
• 6:38
  Christine: And now we have Bend and with Bend the code that you're proving can be the code that your application actually runs.
• 6:48
  Brandon: Yes. And it's like there just doesn't seem to be any downside like because not only is that the case, which is amazing, but one typical issue or difficulty when you use these tools is it takes so long for these formal verification tools to actually verify that whatever things you're trying to verify are true.
• 7:17
  Brandon: It just like is slow but Bend was designed so that the proving can be fast so I am dying to just pull up the homepage of that and start talking about things
• 7:30
  Christine: But before that yeah there's no down side.
• 7:34
  Christine: It sounds also like the agents have changed economics a lot, like previously, the down side of applying formal verification is also because it means that you need to have very specialist knowledge and you have to do a lot of manual proof work. And which can sometimes make it hard to justify for ordinary application code.
• 7:58
  Christine: But I guess now with agents as humans we can probably just decide what really needs to be true and then the agent takes care of the implementation creating the proofs and doing all the other tedious reasoning steps. And then I guess the compiler or proof checker will just check if the proof is actually valid.
• 8:19
  Brandon: And that's exactly how Bend is able to prove things more quickly than these other tools because Victor Taelin and his team when they're working on Bend they knew that agents would be the one writing the proofs and a lot of the affordances that are in let's say, Lean to make it easier for humans to write proofs are really slow.
• 8:43
  Brandon: And so, Bend is just like there's gonna be no fun bells and whistles to help humans write these proofs. It's gonna be extremely manual and annoying.
• 8:51
  Brandon: But agents love extremely manual and annoying tasks.
• 8:56
  Brandon: They destroy them the less features your thing has the more the agents are good at using that tool to, like, solve problems,
• 9:06
  Christine: And that makes sense because often when we build with coding agents, the process is we plan, we set the target or goal, and then the agent will implement, and after the implementation we verify if the thing that the agent built was correct and works as intended. And I guess what's really helpful is that formal verification gives us another kind of machine-checkable gate.
• 9:33
  Christine: It's a very reliable way of verification and maybe even more than test, right?
• 9:40
  Christine: Because or maybe even more than AI instructions. More than everything.
• 9:47
  Brandon: Alright,
• 9:48
  Christine: So I'm very excited to try it out and try applying Bend to my projects.
• 9:55
  Christine: But before that, I'm also curious how Bend and formal verification actually works? Can you maybe in very simple terms or through a very simple example explain a little bit what formal verification is and how it works?
• 10:11
  Brandon: I think the best way to explain formal verification is by talking through sort of this hierarchy of tests, like a testing pyramid, I think, is one way to think about it which I'm gonna put types on as well.
• 10:32
  Brandon: So let's use an example for reversing a string.
• 10:36
  Brandon: This is just like a really simple example so it's a function where if I give it hello I get back O L L E H if I give it empty string I get back empty string, stuff like that so the first thing that we can do is we could add types.
• 10:53
  Brandon: So we could say this is a function that takes a string and returns a string.
• 10:55
  Brandon: And if you do that then if somewhere else your agent tries to call the function on a number, then you're gonna get a compile error.
• 11:08
  Brandon: The type checker's gonna catch it.
• 11:10
  Brandon: Then you can also write tests.
• 11:12
  Brandon: So you can write a unit test which just tests a few examples. So you could say you could write a unit test that says if I pass hello I get back O L L E H, if I pass empty I get back empty.
• 11:27
  Brandon: The problem is, what about Russian characters?
• 11:30
  Brandon: What about emojis? OK?
• 11:34
  Brandon: So to kind of climb the pyramid a bit, we can go to property-based tests.
• 11:37
  Brandon: And in property-based tests you write down properties or laws that make sense for your function. So in this case if you reverse twice, so reverse of reverse of X is the same as X.
• 11:54
  Brandon: For all X. So we write down that property.
• 11:56
  Brandon: In a property-based test, you also describe how to generate random samples that explore the state space in an effective way and then a property-based test will generate lots and lots and lots of examples, effectively doing like a thousand or ten thousand or a hundred thousand unit tests for your function.
• 12:15
  Brandon: So that's more coverage but you don't know for sure that it's working, So if we climb that a little bit more, we can take these laws that we have, like reverse of reverse of X is the same as X and we can formally prove that they're correct.
• 12:35
  Brandon: That's why it's formal verification so the actual computer program that we're using has some understanding of mathematics and it lets us do proofs like a mathematician and say something like I'm gonna prove by induction that the empty string goes to the empty string and when I add a character it means when I'm reversing that character gets added on the other side.
• 13:05
  Brandon: And you can kind of follow the code in a way that explains why it's correct, why it's correctly following that law, like why if you reverse twice you get back the same thing.
• 13:19
  Brandon: And by explaining to the machine giving a proof of this theorem, this law then the computer is able to check that proof is correct and to verify that code does what you want it to do which is kinda crazy that it's even possible to do that so the downside is it's harder and usually slower than as you go up, right?
• 13:50
  Brandon: Like writing unit tests is harder than like just putting a type on there but it might catch some more stuff anyway I'm hand-waving that part finding your laws is sometimes difficult and then but writing a property-based test is harder than a unit test and then doing formal verification and fully proving the correctness of those laws is one step harder but we have AI agents so it's a little easier now.
• 14:21
  Christine: So I guess to understand formal verification, normally a test would ask, can I find an example where this breaks?
• 14:34
  Christine: But a proof can establish that there's no counterexample to the specific property that you proved. So it's a very different approach.
• 14:49
  Brandon: And so when you have a formal proof for that property, you know with a hundred percent certainty that is true.
• 14:58
  Brandon: Which is cool. It's very powerful.
• 15:00
  Christine: Yeah. Very powerful and very reliable. I see.
• 15:03
  Christine: So that's formal verification.
• 15:10
  Christine: What are the good types of things to verify with Bend? Do you have some examples that come to mind?
• 15:18
  Brandon: I think there are things that are obvious which are kind of the edges of your code that are like, manipulating data structures, things that, like, are kind of inherently mathematical.
• 15:33
  Brandon: But if you work with your agent to structure your software around a strong algebraic core, then you can really use it for almost anything.
• 15:46
  Brandon: And that's I think something that is really really exciting and I'm dying to go into. So we have a few examples.
• 15:54
  Brandon: Yeah. Anyway. OK, Yes. So the first thing that all of you should do is you should go and look at Bend's website because it very concisely describes the benefits of Bend so I'll just really quickly run through it.
• 16:13
  Brandon: So I've just shared their homepage.
• 16:16
  Brandon: Bend is a fast language that blocks AI mistakes via proof.
• 16:22
  Brandon: That's what we were talking about.
• 16:24
  Brandon: C-speed, fast. CUDA parallelism, fast. Like you're running on a GPU proofs, like we talked about, and then some nice syntax. OK, cool so runs fast. That's something we haven't talked about yet, but it's really cool so Bend is basically as fast as machine code, more or less, depending on the example plus it can be even faster cuz you can run stuff on GPUs it compiles fast, so it doesn't get in your way anyway I'm not gonna talk about it more than that parallel you can run stuff on GPUs and it blocks mistakes with proofs.
• 17:06
  Brandon: OK.
• 17:08
  Brandon: So, with that in mind, I wanna show you like, OK, hopefully now you have this in your head, like OK, Bend, I can write stuff fast with Bend and I can prove its correctness.
• 17:18
  Brandon: So, I had that floating around in my head and I was like, oh Git is a tool that like developers are using a lot.
• 17:28
  Brandon: Is there something that I can do with Git and with Bend that's interesting? And I wanna show you the conversation that I had with ChatGPT to discover this next project which I'll show
• 17:39
  Christine: Maybe you can look at the steps that you did while building this new project and maybe everyone can then understand what steps are involved.
• 17:49
  Brandon: Yeah, so this is literally what I did when I just wanted to build something with Bend.
• 17:56
  Brandon: So I said, design a project using Bend2 to prove interesting laws for some kind of fast Git implementation and then I sent some other engineering specific stuff and then I said be ambitious.
• 18:14
  Brandon: And I got back something and I had a conversation back and forth with ChatGPT to try and like find something that was both useful, OK, and I'm not gonna share this anymore I wanted something that was useful, fast, and where I can leverage kind of Bend2's interesting provable nature. Right? So something that has like nice laws.
• 18:42
  Brandon: And what I ended up with after my conversation with ChatGPT is a tool that the agent called Proofpack which efficiently calculates the difference between Git objects or any kind of object, but let's just use Git as an example, Git objects that are over here and over here. So as in like there's something in the cloud in our Git project and we wanna pull that down to our laptops or there's something in this folder on our laptop and we wanna have a hundred agents going in parallel and that have slightly different versions that are all committing and pushing and in a world where we have lots of agents that could potentially be working on the same code base at the same time there's actually an opportunity to describe this problem very mathematically using like a set algebra but implement it in a way that can run on GPUs and because it has this mathematical nature, we can state laws and then prove the correctness of those laws. And the thing that's really cool.
• 20:08
  Brandon: Well, so, OK. So let me take a step back. So.
• 20:12
  Christine: There was an opportunity, it made sense to build this with Bend because there's a mathematical way to compute exactly what is missing what kind of objects are missing and compare it.
• 20:25
  Christine: So that's why it made sense to build with Bend.
• 20:27
  Christine: And you also want it fast, of course.
• 20:30
  Brandon: Yeah. And something that we haven't mentioned actually but there's a benefit to using this algebraic structure and stating these algebraic laws even if you're not testing or using it as a verification mechanism.
• 20:49
  Brandon: You obviously should use it as a verification mechanism because it guides your agents.
• 20:53
  Brandon: But there's another benefit. OK Each law unlocks a kind of freedom for an equivalence it's sort of a freedom for the, like, user of that code or the implementer of that code to make choices that do something different.
• 21:18
  Brandon: For example, optimize.
• 21:18
  Brandon: So there's like a basic law is associativity. So that's like I'll state it just on addition with integers. So if it like if I have X plus Y plus Z, I can like draw the parentheses around X plus Y and then plus Z.
• 21:35
  Brandon: Or I can draw the parentheses around Y plus Z and it's still like X plus parentheses Y plus Z.
• 21:41
  Brandon: Yeah. So those two are the same for addition and for lots of operations. And when those two are the same, it means I have the freedom to write that code in two different ways or to put it another way, I can parenthesize however I want.
• 21:57
  Brandon: Or to put it in another way, if I have a lot of things that I'm doing and I'm free to parenthesize however I want, I can choose to run it sequentially one at a time or I could push it to a GPU and run lots of stuff all in parallel and kind of combine them together. Yeah.
• 22:20
  Christine: So, projects where things do not need to happen sequentially are also a good place to apply Bend.
• 22:27
  Brandon: You might not know that until you think through the algebraic structure and figure out the laws.
• 22:34
  Brandon: Like whenever you discover that there's associativity, you unlock parallelism it may not be obvious at the start of your sort of brainstorming about even this problem like it's not obvious that there's a way to compute maybe it is to other people but there's a way to compute like the set of things there's a set of things that exist, there's a set of things I have and a set of things that are over there, and like what are the exact things that I need and send them to me like that computation is not obviously parallel, but if you think carefully about the algebraic structure and you write down a law and then you prove that the law is correct, like and you're not wrong about your law, then it's safe to do parallelism.
• 23:23
  Brandon: And that's just one example, but different laws enable different kinds of optimizations in your software. And this is important when you're building something fast
• 23:39
  Christine: Very clear steps to start with.
• 23:41
  Christine: So do they start with trying to make sense what project to apply Bend to or do they start with laws?
• 23:49
  Brandon: So Bend aims to be a general-purpose programming language that you can use for anything.
• 23:55
  Brandon: So, you can use it for anything.
• 23:58
  Christine: Yeah, so you start on a higher level, right?
• 24:00
  Christine: Like, OK, I think using formal verification here might make sense. I think you could represent things using algebra. I think there's some opportunity to run things in parallel.
• 24:14
  Christine: And are these like the right questions to ask as a first step when people are going to build a new project and when people are deciding am I going to use Bend or not?
• 24:23
  Brandon: Yeah, I think at the high level Bend has a nice type system, it's nice functional code, and it has this formal verification layer.
• 24:37
  Brandon: So even if you're only using parts of it, it's like, in theory, a better tool for your agents to use to build any kind of software in practice, it's also a brand new programming language. There's not a fully fleshed-out standard library. There might be little bugs here and there.
• 24:55
  Brandon: And so, like, tomorrow, it might not be the best choice for any random project.
• 25:03
  Brandon: So, with that in mind, I would actually suggest the following process.
• 25:12
  Brandon: Before you choose the programming language, before you choose your tech stack, figure out your idea and work with your agent to come up with the algebraic structure.
• 25:19
  Brandon: And then, at that point, you can have a conversation with your agent and decide, OK, I'll build this in Rust or maybe I'll try Bend.
• 25:32
  Christine: So it sounds like you start with a problem and you find a part where there's a mathematical shape and you can do this with the agent.
• 25:44
  Christine: And then you talk with the agent through the algebraic structure and the laws just by using English. So you do not need to like write the mathematical equations.
• 25:57
  Christine: You mentioned Proofpack. Could you show this step in your process, your building process?
• 26:03
  Brandon: Yeah, so I had that ChatGPT conversation.
• 26:08
  Brandon: And then at the end of that I got a spec out.
• 26:11
  Brandon: I did a lot of grilling.
• 26:13
  Brandon: I got a spec out, and then I just gave the spec to Opus 5.5 and I said use Bend make it fast, make the laws work, go.
• 26:22
  Brandon: And that's it.
• 26:26
  Christine: Interesting. And then I guess you had an idea what you wanted to build and then you said you talked with the agents through the algebraic structures and the laws. So how did that go?
• 26:38
  Christine: What did you exactly ask and how did that back and forth look like from your memory
• 26:45
  Brandon: I can pull it up cuz I did that in ChatGPT I didn't steer at all.
• 26:51
  Brandon: I just sort of said like what are the laws we can find here? Once I did the grilling and I got the right shape of the project ChatGPT just suggested laws to me.
• 27:02
  Brandon: And I'm like, OK.
• 27:03
  Brandon: These are great so I can find some of them.
• 27:10
  Christine: Wait, so when you say you did the grilling, so you mean you had the problem, you found a mathematical shape, and then you also did the grilling, so you had some back and forth with the agents, so the agent really understood what you wanted to build. And then the agent just suggested the algebraic structure and the laws, and you didn't push back on that a lot. Is that what you're saying?
• 27:31
  Christine: Yeah.
• 27:31
  Brandon: Yeah.
• 27:32
  Christine: OK.
• 27:32
  Brandon: Correct. And this is sort of a vibe-coded project, so a vibe-lawed project.
• 27:37
  Brandon: So like everything there's a degree that you can go deep on and there's a degree you can just go hands off and let your agents do it but I think this is important, like I personally loved like thinking carefully about problems, coming up with the algebraic structure and then finding the laws that's like something that I used to do, like since twenty fifteen like all the time when I think about software I was doing that manually before LLMs and even me, I'm just letting my agents do it I'm trying to understand them and maybe I'll like push them depending on the project.
• 28:21
  Brandon: But I think it's really OK to just kind of steer the agents in this direction, saying like, OK, find this algebraic core, find these laws, what do these laws unlock, what do these laws enable, what optimizations do they enable, how can we leverage these optimizations and it's this thing that we talked about two videos ago in the fall workflow. You want to make your intent clear, but you don't wanna prescribe a specific direction because the frontier models are smarter than you now.
• 28:52
  Brandon: And you have to stop fighting that.
• 28:54
  Brandon: You shouldn't say like, I figured out the laws, it's these five. You shouldn't even say, I think it's these five because then that'll like that'll fix the agents down a path.
• 29:03
  Brandon: It's more like, OK, is everything I said?
• 29:06
  Brandon: You wanna give them that guidance and that freedom to explore and discover those laws.
• 29:12
  Christine: You communicate the intent and the agent who is really smart will come up with the suggested approach or implementation. And I guess you could also use a strong reasoning model to pressure test the laws and maybe looking for missing edge cases to make sure that the intent is really really clear.
• 29:32
  Christine: So does this require deep math knowledge or can someone without that background still get value from or still do this step.
• 29:44
  Brandon: If you look at my old presentations, even before LLMs you only need really middle school algebra to get started. But now with LLMs you need elementary school English to get started.
• 29:58
  Brandon: And you don't need any math background.
• 30:01
  Brandon: So that's what I'll say.
• 30:01
  Christine: Do you have the history of this part of your session? Your coding session?
• 30:07
  Brandon: Yep. Here's my prompt.
• 30:07
  Brandon: I'll share so we started with a vague idea, we did a back and forth, an interview where the agents discussing the mathematical shapes, I'm asking questions, trying to understand it the model said, hey, like, there's actually this cool generic theorem that works on any kind of objects, not just Git and I was like, cool, OK and then we explored other ideas that were dead ends.
• 30:38
  Brandon: And so now I'm at the point where I have a direction and I wanna come up with like a spec for that direction with the laws and the algebraic structure and I just collapsed that into one step in this in this example.
• 30:59
  Brandon: So I'll skim read like this prompt so I said we wanna start with the generic theorem underneath everything, the laws on top of it, and interesting bits so that we can start using it for real with Git in Bend2 give me a clear product and engineering document that's self-contained that I can give to my engineer specify at a high level the kinds of laws we want and what optimizations they unlock so we make sure that we build it from the start with a compositional algebraic core that we can prove nice things about. And then we can use the high-performance Metal, that's the parallel Mac substrate, of Bend2 as well and then I gave it some extra little bells and whistles to push it in the right direction I don't know if we need to go into that so, well I'll just say, I said the words denotational semantics.
• 31:56
  Brandon: Google it if you want, but it pushes the agents in the right direction also and that's it. I got a bunch of proof obligations, that's like unproven laws and an engineering spec and product spec based on the result of that conversation I had.
• 32:14
  Brandon: And then I fed that into Opus and said build it
• 32:17
  Christine: Cool. Can you scroll down?
• 32:20
  Christine: I guess this equation it describes some behavior that you defined for the project that you want to build.
• 32:31
  Christine: What I'm hearing is you do not need to check if the math is correct but you might want to check if this representation really reflects your intent.
• 32:42
  Brandon: Yes, that is important.
• 32:42
  Brandon: That is very important but I think it's okay to trust the agent's English translation of the math to get that intent across so if you can see my screen, it's saying like in words, a proposed addition covers the requirement exactly when it includes every missing required object. Which is a little abstract, but you can also read this as like if I require ten things and it includes all ten things, then I have the things that are required.
• 33:21
  Brandon: Whatever. Right. It's straightforward.
• 33:22
  Christine: So basically in the step when the agent gives back a technical spec and also its approach for what laws and what algebraic structures to apply, basically you just review these intermediate deliverables in the same way how you would normally review plans before the agent starts building.
• 33:52
  Brandon: Yes. That's a concise way to put it.
• 33:55
  Brandon: Thank you yeah. So.
• 33:58
  Christine: Alright, cool. And what comes after this?
• 34:02
  Christine: My question is, did you have to respond here?
• 34:05
  Christine: Did you have to correct things here?
• 34:06
  Christine: And then, if not, now you just give this, you copy paste it and give it to your implementation agent?
• 34:15
  Brandon: Yeah, so I take that plan with all the laws in it And I gave it to my implementation agent, Opus 5.5, I think, was new, so it just was like, let's use Opus and, oh, the other thing that's interesting to know Anthropic trains the Claude series of models on Bend and on the theoretical kind of underpinnings of Bend.
• 34:44
  Brandon: And the Codex series of models are not trained on Bend.
• 34:56
  Brandon: I assume this will change soon but this means that the Anthropic models are way better at working with Bend, like understanding how it works and then proving with it for now. So this is alpha, OK?
• 35:14
  Brandon: Like you all should be listening intently here, alright so this is why there's value in having access to lots of different frontier models ChatGPT is really good at math and it's way better than the Anthropic models at math. OK? I know both of the frontier labs are proving like interesting mathematical theorems that have been unsolved for a long time. But the Codex models are ahead.
• 35:45
  Brandon: So like if we're trying to come up with math that underpins like our software, then it's better to use the Codex models.
• 35:55
  Brandon: It's better to use ChatGPT.
• 35:59
  Brandon: And if you have ChatGPT Pro, if you have the highest tier of subscription for Codex, you'll have access to that That's the best model in the world at math.
• 36:10
  Brandon: So, plan in that.
• 36:14
  Brandon: Make your math in that at the math level.
• 36:19
  Brandon: But then take that plan Yeah. I would recommend that in ChatGPT Yeah. If you have access.
• 36:30
  Brandon: Or whatever the highest Astra tier that you have access to for the math part, you could.
• 36:35
  Christine: Is that also the model that has the highest benchmarks? For math?
• 36:40
  Brandon: Yes. Yeah. So you could probably look at FrontierMath benchmarks and find that I don't know if that's still true. There's kind of a vibe, like a vibe with mathematicians that doesn't always follow the benchmarks. But the current vibe as of date of recording, end of September twenty twenty-six, the ChatGPT Pro is the best at math.
• 37:07
  Brandon: OK. So once you have your math figured out and you have your plan, that you could do in Fable if you wanna do separately. I just did it at the same time.
• 37:16
  Brandon: Then at the implementation, if you're using Bend, then get to Anthropic as quickly as possible. Cuz the Anthropic models are trained on the core underlying type theory that powers Bend, which is like insanely cool But out of scope for this conversation OK. So that's a long-winded way of saying I now switch to Claude and Opus.
• 37:39
  Brandon: This is where I don't know where my session is but I just said do it.
• 37:44
  Brandon: Implement this, and pasted the plan.
• 37:47
  Brandon: Right? What I got back it only took a few hours or something.
• 37:52
  Brandon: I got back something that seemed to work and Opus said I proved ten of these twenty laws. And the other ten I just put in this other file cuz I wanna do it later cuz they're too hard.
• 38:07
  Brandon: So I was like, no, prove all of them and then it took another thirty-six hours so to get all the proofs.
• 38:16
  Brandon: And twenty laws turned into a hundred ninety.
• 38:23
  Brandon: Because some of them were so big that they were like hard to prove altogether and so they were broken up into pieces but the interesting thing is yeah I can generate some kind of visualization and then we can stick it in the video.
• 38:45
  Brandon: I don't have one off the tip of my hand. So let's like in the future I will make that and I'll show it and look! Oh my god, look at all these cool theorems that we proved.
• 39:00
  Brandon: Yeah. So it's ostensibly the same twenty or so that, like, we originally came up with ChatGPT but a lot of them were broken up into pieces.
• 39:09
  Brandon: And really interestingly, four of the original twenty were false.
• 39:16
  Brandon: So the math was wrong so they were not just false as in Claude failed to prove them.
• 39:25
  Brandon: They were false as in there was a proof that they were false. So there's a counter example as like one way to do that. So there's a way to construct like a specific starting state that can kind of disprove that law and that helped change the application slightly. So the laws in place proving the laws steered the software to be more correct, which is cool it turns out, thank God, the laws that were false didn't break the whole project.
• 40:06
  Brandon: There were some kind of specific edge cases that needed to be stated in the right way, and those edge cases have to be in the code as well for the code to be proven correct.
• 40:14
  Brandon: Those specific details don't matter of like what those were, but the point is like the process of proving the laws, not just writing them down, actually found bugs and then made the code better.
• 40:28
  Brandon: So that's really cool.
• 40:30
  Christine: Cool. So the proof failed and then the agent got like really strong feedback and they did have to repair the bug
• 40:41
  Brandon: Yeah the models are really smart and so they like did a lot of thinking, tried a lot of things and figured out that there was a counter example and fixed it. Yeah.
• 40:54
  Christine: Right and then you ended up with your Git state calculator that is really reliable and computes exactly what is missing and could also do it quickly. Yeah,
• 41:08
  Brandon: The cool thing about Bend is the same code can run on CPU or GPU and on a machine like a Mac where the memory is shared between CPUs and GPUs, you can in Bend, like, do some logic on the CPU and then not do any copies to the GPU.
• 41:27
  Brandon: You just kind of switch to GPU code and acts on the same data. So in other words, it's just like really really effective at these kinds of like heterogeneous workloads where you're switching between CPU and GPU and you can prove correctness which is really cool. So yeah, so my tool in theory if there's enough contention would speed up if you ran it on the GPU, but it turned out that at like any reasonable number, like a thousand concurrent agents using the same Git state, it's faster to just stay on CPU
• 42:01
  Christine: Awesome. OK, it was very helpful to walk through the steps around how to build a new project from scratch with Bend.
• 42:10
  Christine: Did you also use Bend for other projects?
• 42:19
  Brandon: Yeah, So I tried well, our podcast video editor that we built for this podcast.
• 42:28
  Brandon: We have an amazing editor who's helping us now but we still use it for short videos this video editor has a strong algebraic core, cuz I love doing that in all of my software and part of it describes how to make safe cuts.
• 42:51
  Brandon: So think like if I wanna cut all the “ums” out am I cutting all the waveform, not leaving a little bit so there's a click if there's two cuts near each other can we combine them? So all these rules are expressed as laws.
• 43:07
  Brandon: And it's already set up that way and there's this interesting feature of Bend that not enough people are talking about but is really powerful. OK? Alpha alert.
• 43:20
  Brandon: Pay attention. OK Bend, yes, it can compile to fast native code, yes it can compile to GPUs.
• 43:28
  Brandon: It also compiles to the web, compiles to JavaScript.
• 43:32
  Brandon: And that means if you have any project that uses TypeScript or that is in the browser, you can write part of it in Bend.
• 43:40
  Brandon: So you can take an existing project, take some slice of it, and rewrite that in Bend, and then prove correctness of laws around that part of your software.
• 43:50
  Brandon: And that's exactly what I wanted to try, and I did try, and it worked and it's awesome.
• 43:54
  Brandon: So basically the part of the code that uses this algebraic core and these laws to do an efficient solve I looked at that again with Opus 5.5 and said, OK, let's like revisit this, let's use Bend.
• 44:16
  Brandon: And I was able to rewrite it in Bend, replace that whole code, it's out it's replaced with Bend and it's like pushed and we use it now and the process of examining it and rewriting it in Bend and getting the laws proven helped speed up that code by like four X.
• 44:36
  Brandon: So what used to take one and a half seconds and probably was buggy to be honest now is definitely correct, proven correct and fast. It's like three hundred milliseconds for like solving cuts on an episode that used to take one point five seconds
• 44:55
  Christine: Wow. So Bend can compile to JavaScript, native targets and you can replace one kernel inside an existing TypeScript project without rewriting the whole app. That's cool.
• 45:08
  Brandon: It's amazing. It's amazing. So I think it's important just to know that you can do that so you don't have to just save Bend for like hardcore systems projects where you're wanting to do something really fast but any kind of web project even a web project that like you wanna use React, you wanna use that stack that I talked about a few episodes ago with like TypeScript, Bun, Oxlint, Effect, et cetera but maybe part of it really has a strong algebraic core and strong laws and it's important and correctness is important and you're struggling with it you can take that slice and rewrite it in Bend. And that works today and it's great.
• 45:54
  Christine: Cool. And are there also like moments when you should not use Bend?
• 46:01
  Brandon: Yeah, so I still think what I said last time is still true, like default to TypeScript, sometimes you use Rust but Bend is interesting it's brand new so all these things I'm like singing its praises.
• 46:20
  Brandon: It's not perfect I ran into bugs in Bend, the Bend compiler itself.
• 46:27
  Brandon: There's a lot of standard library things that you'd want that are missing but the thing is like your agent can work around those. So it's not that bad but yeah I would say like Bend is something that I really strongly recommend everyone plays with so you can get a taste of the future and for some experiments you should use it now for internal tools things that you don't have to worry about maintaining for a while the language will probably evolve you can use it today but then I think your skills of being able to prove your code, working with your agents around these laws, these algebraic structures, it's gonna improve your software in other languages and it's a bet that Bend will stay around and will just get more and more popular and more stable and bigger standard library. And then it might become one of those instead of just TypeScript or Rust you might be like why am I not using Bend?
• 47:25
  Brandon: And maybe my default is Bend and I fall back to TypeScript.
• 47:29
  Christine: Right. It's very exciting to see how the Bend ecosystem will evolve from here Yeah it's still very early and young going back to like when to use Bend and when not to use Bend, are there any specific, use cases or situations where you're like, well, then it's actually not suitable to use Bend?
• 47:50
  Brandon: I think you don't wanna use Bend for your whole web app yet I think there's not enough like mature like user interface libraries and there's certain like floating point operations are not something that are easy to work with in Bend.
• 48:14
  Brandon: So if your application needs those there's like little edges around the language which your agents can help you discover and then like I said if you're writing software for a bank like don't pull in the Bend dependency yet but for personal projects for playing with stuff I think it's ready to use now and it's fun and different. And that's really really exciting.
• 48:44
  Christine: And is there still a trade-off between like the benefits from Bend and the cost, maybe in terms of compute or maybe just effort and time that you put into it?
• 48:57
  Brandon: It uses more tokens.
• 48:57
  Brandon: Yeah you need more tokens because the models don't know Bend as well as TypeScript you need more tokens to prove laws instead of just test them in exchange you get something that is like more correct and that steers your agents better.
• 49:23
  Brandon: So if you're trying to save tokens, you probably shouldn't be proving lots of laws in Bend.
• 49:29
  Brandon: Like I said, that Git application that I made it took a few hours to build it and then thirty-six hours to get all the laws proven.
• 49:42
  Brandon: I'm answering all your questions with like the positive spin. I'm just very excited about it and I recommend everyone try it there are some rough edges but like you have agents so it's fine. That's my version.
• 49:54
  Christine: How far should people go with verification?
• 49:59
  Christine: So you talked about that pyramid or ladder for verification and the strongest one is probably Bend.
• 50:06
  Christine: But how much verification do projects actually need?
• 50:11
  Brandon: I think you can think about this in the same way as testing. It's like how many tests do you need?
• 50:16
  Brandon: How many different kinds of tests do you need It depends on how big your project is.
• 50:26
  Christine: Right. So it could be overkill sometimes.
• 50:30
  Brandon: Yes. Yeah So in the same way that it's overkill to write like thousands of different kinds of tests for very simple code, it's overkill to prove lots of things about lots of your code when only part of it is the really complicated part where agents are tripping up or where you're gonna evolve often so yeah I think the same way you can also use Bend and not prove laws but yeah
• 50:59
  Christine: There are some operations that are like key to get really right, otherwise the editor would just be useless. And those are the parts where you applied Bend.
• 51:09
  Brandon: Yes.
• 51:10
  Christine: OK. Yeah, that hundred percent makes sense.
• 51:13
  Christine: So I think what I'm taking away from this episode is actually bigger than just Bend.
• 51:20
  Christine: It feels like as agents write more code for us, we need to get better at being really clear about what has to be true and giving agents ways to check that themselves so they can run more autonomously.
• 51:34
  Christine: And Bend is very early, but it's a very interesting example of what that could look like.
• 51:42
  Christine: So I hope that people listening got something out of this episode. And if you try it out on something, please share it with us.
• 51:49
  Christine: We'd love to see what everyone is building with Bend and what kinds of things you have decided are worth proving with Bend.
• 51:57
  Christine: So this is the Superlinear podcast.
• 52:00
  Christine: Every week we share one emerging practice for building with coding agents so you can stay ahead of how this craft is changing and figure out what's actually worth trying. We'll be back next week with another one. See you then.
• 52:14
  Brandon: Bye everyone.