Now more than ever: building reliable software in the age of agents | Ron Minsky | Bug Bash 2026

0:01 I mean, there's no better presentation software on the planet. It's really, you know, variable width fonts in terminals is what we've all been waiting for. Um, okay. So, you you know how like there's like an old somewhat over the hill person who like the world changes in some dramatic way and they use it as an excuse to say, you know what, now more than ever, all that stuff I always believed and told you, it's now now is the time to do it even more. So like somewhat awkwardly this is that talk and I'm going to um and the talk is going to be like there's a lot of smart people here who've said a lot of things I agree with. The last talk from Ben I think had a lot of stuff that really resonated with me. Um and so I'm going to try and lean like Jane Street's kind of technically a pretty weird place and I'm going to try and lean into the weird and focus on the kinds of questions and the kinds of approaches that are a little different at Jane Street than they are at other places. And so to start with, let me just say like a few words about like what Jane Street is and what it's like and then we'll talk more about the actual substance.

1:03 Okay. So what is Jane Street? So we are a global trading firm. More than 200 trading venues, more than 45 different countries. Um a lot of people when I started there was about 35 people. There's now about 3,500 people which is kind of terrifying. And like maybe 2,000 of those people write codes on a regular basis as part of their ordinary job. Um, some of those are like software engineers, some of those are traders, some of those are like all sorts of people in different spots. Um, and there's like a lot of trading activity.

1:32 We're just like it's kind of I mean I remember like even very very early in the day I remember like there was like a trading system that that I had built that was on its own trading a tenth of a percent of the New York Stock Exchange volume. And I remember thinking, "Wow, that seems unlikely." like I very surprised that that is true and seemingly making money and like I don't know things have grown since then uh these days we are something like 10% of the US equity market maybe 8% of US options market maybe 20% of European ETF markets um and I could say another bunch of stats about how big we are but like it all sums up to we trade hundreds of billions of dollars a day which is of course terrifying right here we are software engineers a lot of us right What unifies software engineers? We are terrible at writing programs, right?

2:24 They're not. It's very hard to do, right? You write these programs that like always, frustratingly only do what you wrote down and not what you meant, right? Um and so the whole thing of like we are going to like write a bunch of programs and hook them into the market and our bank account at the same time is like that's a scary thing. Um and as a result it is a place that has a strong commitment to rigorous engineering right it really matters to us to get things right I should say like not in a way that's like independent of value right there are lots of parts of the things that you do where like correctness matters less and it's actually very very important to vary the work and scrutiny and care that you apply to different systems in a way that's just like sensitive to the costs of the different things involved. Um, another thing about James Street is like we're pretty AI pilled, right? We, you know, this, you know, this machine learning thing like I think it's going to be big. Um, so we have like heavy adoption and deployment of AI agents throughout our stack. Um, we actually like spun up an AI assistant team several years ago to build tooling to make it great for software engineers to use agents and LLMs and all of that to build software. Um, and they were kind of awful, right? Like the actual like agents weren't smart enough. And I like I think my overall estimate for most of that time is that it was a net drain on productivity. You both had a bunch of talented people building the infrastructure and then the people who were using it were like maybe getting some benefit and maybe not. And like I think you know but like last November it's like oh wait it like crossed the threshold right and suddenly the models were good and like it's like building a sailboat when the wind's not blowing and you know it didn't blow for a long time and then suddenly the wind started blowing and so it feels very different now and uptake on these things has been very strong and in some sense what this talk is about is like you know there's a whole new world software engineering is different I like I am responsible for some leadership in the kind developer tools area and a thing I go around telling people is like we're all AI assistants now right like just co so just the agent the agentic work is constitu enough of the process of software engineering that when you are building tools for people to do software engineering you have to be thinking about the AI overlay or you're just kind of not doing your job um we also do a lot of developing novel ML architectures and models for our own trading that kind of not for like a human to use to help them be more efficient at But like something that produces values that help guide the decisions of an automated trading system. Uh and this is now driven by shocking numbers of dollars of uh compute infrastructure that we have thrown into this. So it's like a huge systems project, right?

5:12 That's like the thing about ML, right? Is like there's some math for sure and that's very important, but there's also huge systems problems that kind of come along with that because scaling and performance is so important in machine learning. We're also very plilled, right? We have a speaking of ways that James Street is weird. Uh we uh use Okamel, a comically uh unpopular programming language as our primary language for doing serious software engineering. Uh we also use Python for machine learning and data oriented scripting because we're not totally nuts. Um and there's a lot of adoption throughout the organization of like ideas from programming languages. Uh it's just kind of a a thing that we care a ton about and think a lot about. Um and even more weirdly we have you know we thought you know Okamel not unpopular enough. Uh let's make our own like cool extensions to the language and make it better for our use cases. Um so anyway this gives you like some sense of the kind of engineering approach that we have in the kind of ways that we uh that we approach all these kind of problems.

6:13 And if you're interested in the ox camel thing itself, it's like in some sense we've had this for quite a while now, but we've relatively recently tried to make it easy for other people to try out and to learn about. Um, we even have documentation of the of the language extensions shockingly. Um, and so yeah, you can just like go online and and grab it and learn about it and try it out. Okay, so what do I want to talk about? I want to talk about a bunch of the ways in which software engineering hasn't changed or rather maybe to put it more precisely a bunch of ways in which a lot of the things that have always been important have become some mix of more and differently important in the world of agentic programming. And again I'm going to try and focus on some of the ways in which our approaches are somewhat unusual. Uh and I'm going to kind of focus on three areas. Type systems testing uh and code review. Um, so let's start with types. Like why should we care about type systems in the first place? Um, so one kind of amazing awesome thing about type systems is they just let you clear out and eliminate a huge class of bugs just kind of out of the box without having to think very hard or try very hard. Like the system by itself fixes a bunch of bugs and important ones. If you program in O camel, you just don't get any null pointer errors, right? This is, you know, the old billion-dollar mistake of having nulls implicit everywhere in your programming language. Like, we just don't have to live that way, right? You could just have a programming language that solves that in a fundamental way.

7:45 We get no out of bounds errors, right? There's all these great research studies from Google and Microsoft that like 70% of their security vulnerabilities are just like memory errors that should be a solved problem, but because they are using just the wrong programming languages, you still have these security problems, right? Um, and then we have with our own like extended weirdo version of the language, we have some extra stuff. We can have safe stack allocation. So, it turns out you don't always want to use the garbage collector. Sometimes you want to do stack allocation. And there are lots of languages that support it. C and C++ support it. And how do you do it safely?

8:22 You're very careful, right? You know, the plan is don't get it wrong, right? Um, and Rust actually has type safe stack allocation and so does OCL now. Um, we also have data race prevention. So you can have guarantees just kind of baked in there that you can write a parallel program and you know that that program will not have any data races. Um, but it's not just these kind of broad classes of kind of bakedin protections that you get from a type system. It also gives you lots of freedom to enforce application specific invariance. And I think an important kind of leveling up that you get as a software engineer who uses a a language with a type system that is rich enough to do this kind of work is where you stop thinking of the type system as like a kind of nanny process that hovers over you and like slaps your hand when you make a mistake and you start thinking of types as part of the design process.

9:19 Right? it is part of the way in which you think about express enforce structure the invariance of your program right and I think that's a it's a it's a powerful difference you get a certain amount out of the box but you get much more if you think of the type system as a tool uh and and I think there's like a common feeling people have about type systems that like oh it's just about like does do like do the pipes fit in together in the right way did I pass a floatingoint number where I meant to pass a floatingoint number Um, and this is, I think, just a dramatic underappreciation of the power of type systems. And some of what I want to do is to just walk through a little bit what are some kinds of examples of how you can leverage type systems to do more than just like make sure that the pipes connect correctly.

10:04 All right. So, let's just to start with like a concrete example. XXS errors like cross-sight scripting. you if you prefer you could think about this as like an example about uh SQL injection attacks but it's like a classic relatively straightforward pretty common security mistake that people make and it's like super easy to make the mistake. Here's a little piece of code in Okamel that like thacks together a part of a web page by taking some arguments that are strings and like slamming them in using a kind of uh string interpolation uh syntax and generating the output. And of course that has unescaped user input. There could be all sorts of fun stuff sitting in those strings, right? Little little Bobby Tables lives uh in this example.

10:51 Um so this is like not ideal. Now, of course, you can write the correct code. It is not hard to write the correct code. You just have to have the right escaping function and call it. But of course, it's much better to build your system so the mistake can't be made. So rather than doing the work every time you construct a piece of HTML to make sure that you do the right escaping, what you really want to do is make the mistake impossible to capture it at the type level. And like that's actually relatively straightforward. This is what the same code would look like in like the actual web the actual Okamel web framework that we use at Jane Street.

11:27 Uh, and if you look there, it doesn't look super different. It has like percent HTML which actually like just triggers a a different code path than the percent string stuff. Um, and critically you see it has that like node.ext thing and node.ext in fact does the necessary escaping. If you're used to like the React world, there's also a syntax which is a little more concise that just kind of does it for you by default, but sometimes you want to have more explicit control. But the key thing here is if you don't put node.ext in, you will get a type error, right? And I think it's important to like understand that if you look at these examples just kind of on their own on the screen, they all feel a little trivial because it's like a tiny little piece of code and all the things you have to get right, you know, locally you could just get right.

12:11 But the important thing about types is the kind of spooky action at a distance. You can have many layers of code, you know, that along the way and the the the mistake can be made in all sorts of different places, but the types are a kind of global system that tie the invariants together and make sure that you make the mistake nowhere. Right? So that's another one little example. Another one is here's another one. Uh I kind of sort of by mistake at some point invented a weird catchphrase make illegal states unrepresentable. So this is like a network config oriented example around that. So here is a type that uh is like a simplified version of a real type that we have in our codebase. We have a team that builds a lot of automation around network configurations and it does kind of software defined networking in in various forms. Uh and of course you need types that represent the configuration of your network switch and your network interface here. And this the way this is structured is a way that kind of mirrors what actually happens in the switch configs where you have these kind of sequence of commands that kind of basically set various configuration parameters. And so you kind of model it straightforwardly. This command.t type is what's called a variant. So it's a disjunction. It's either an MTU specification or it says the interface is shut down or it gives you an IP address. And then you kind of wrap that up into a larger type that tells you the shape of the overall thing. And and what's somewhat awkward about this is that there's a lot of ways of getting it wrong, which is to say the MTU thing can only be said once, right? You're only allowed to you're only allowed to declare the MT the maximum transmission unit or minimum minimum transmission once. Uh max, sorry, thank you. Um you only split like it would be weird to say shut down true, shutdown false. You should just say it once. The IP address, however, you can say multiple times, right? So this leads to weird code, right? So here is a function that computes the effective MTU. Um, and it first computes whether it's shut down and if it's shut down, then it just doesn't give you back an answer. And if it's not shut down, it kind of looks through and sees if it finds the first MTU declaration and returns it to you.

14:22 And otherwise, it returns none. So it's like not a very complicated piece of code but it's like kind of subtly wrong which is to say this is shutdown thing like is it right to say that it is shut down if the shutdown thing appears twice like what is the semantics on your switch if you say it two different times right and similar with the MTU thing like is it correct to just pick pick the first one maybe the actual enforced one is the last one so the code is kind of in a somewhat non-obvious way not really correct um and you could like write code that was more sensible that like went through and looked for the bad condition and on the bad condition errored. But an even better thing is to make the bad condition impossible. So here's just a way of rewriting that. So now you have this one type interface.t and it instead lifts into record fields all the things that were previously as commands. Some of those things are optional. The ones that are allowed to be specified zero or one time are optional. Those things that can be specified an arbitrary number of times are represented as a list. And now the code that you end up with is simpler and better than the code before. It's like easier to read. You can't make the weird mistake here. Um, and again there's the kind of spooky action at a distance thing is important. The type is defined in one place and like it's on the same slide, but the code that's doing the computation could be anywhere, right? So you can simplify code across your codebase by making changes in a kind of localized kernel where you pick the right shape of the data.

15:50 So that was all about why types are important and why they matter in the kind of ordinary traditional software engineering context in our new agentic world like what does this change? So I think one critical observation about agents is they thrive on feedback right and this is actually a true fact both in you in using the models like when you are off running them and they are running tools and all of that they need to get feedback in order to do their job well and also in the training process right in order to train the models to do good things we need to provide them with feedback um and the feedback serves multiple purposes there's a kind of just in time context that that is useful like the models are actually quite limited in the amount of context that they can absorb at a given time. A million tokens sounds like a lot, but it kind of isn't.

16:41 There's lots of things you want the models to know and it is hard to pack them all in there. And one nice thing about the type system is that you know you write a piece of code and it suddenly gives you a lot of information when there's a type error and also you can like give the agents tools to look at code and pull up the types and those types themselves are very informative. So this kind of feedback that comes up when you need it is very valuable to the models. Also, it's really fast, right?

17:07 You should have fast test suites, but this is faster than any of your test suites. These static analyses that kind of live in the middle of the type system tend to be very quick, right? And I think that helps you have more efficient agent harnesses. Um, and this is really valuable for the agents because as we were talking about the L the LLMs maybe not so different from people are stochcastic and they have bounded memory and the rigor that you can get in a type system provides a kind of consistency that the models at least in the present day are not very good at providing on their own. like you can like tell the models like which invocation it's supposed to do of the build tool at the beginning and like 230,000 tokens later it may not remember it, right? Much less the complicated crosscutting invariance of the system that you're building. And so being able to express the things that are important that are structural about your code in a kind of rigorous way that the models can see has a lot of value.

18:04 And the kind of thing I was talking before about being able to do application specific invariance is very important. You get to write small typed kernels that can enforce global rules across your whole codebase. And as a lot of people have been saying verification is now the key bottleneck. And the other thing that you get out of types is it helps humans understand the system that's being used and the code that's under construction. uh they provide and the types are just kind of provide basic and necessary assurance.

18:39 All right, so that's most of what I want to say about types. Let's talk about testing and like what do we do for testing? Like we do all the things, right? There's we do classic unit tests, property based tests with quick check, fuzzing with AFL, full system deterministic simulation testing with antithesis is a relatively new addition to our to our uh set of tools. Um, we sometimes run sideby-side comparisons of prod and dev to make sure that the new system is doing what it's supposed to be doing. We have test beds where we get to do replays of historical data and so on and so forth. Like we do a lot of different kinds of testing and in some sense I think most of this will be pretty uncontroversial to this room that like these are good and useful things to do. Um, so I want to talk about a thing that we do that's kind of weird and why I think it's both good in the present and in the future world. Um, and in particular, we do a lot of what what I'm going to describe is what we call expect tests. It's a particular idiom I'll kind of describe in a second. Um, and we also do a lot of not whole system but library level deterministic simulation. And I want to talk about why I think there are like some quite strong advantages to doing it in this library level way above and beyond the value you get from an antithesis style solution.

19:53 So what is an expect test? Um the basic idea is you have these tests where you print stuff out and then you can capture the output of the printing in the text. And like I think the first and most important thing to know about these is it sounds like kind of a bad idea. Like it's not obvious why this is a good way to write tests. Um people worry that it encourages like a lot of laziness. It's like when I write a test I don't need to think about the properties. I just like see what it does. I like write some behavior down and it prints some things out and I look at it and think looks good to me and now I think I've tested something. So that sounds kind of bad.

20:33 Um, and it also it I I want to be careful how I say this. It's not that you can't do property testing in the context of expect test and we totally do do property testing but in some sense the primary thing the direction it encourages you is to do example-based tests rather than property tests right and like I thought we all agreed that property tests were better. So like why is this a good idea? Um but actually even though it all sounds like a bad idea expect tests are awesome. like they are at their best a tool for driving human understanding of the program under study and I think that's just an incredibly valuable thing. Uh and like all the benefits of other testing approaches are very real but this kind of understanding component is huge and I think at the heart of why we really like expect tests.

21:24 All right so let's give some examples because I think it's very hard to think about a testing framework without seeing how it might work. Uh so here's like a weird little example of an expect test. Uh so this like declaration at the top let percent expect test is like that percent expect test is the thing that like triggers off some like magic syntax transformations that kind of make this whole system work. And basically you see like a chunk of code and that's just like ordinary code just like dispatching some code that's doing something. And then percent expect is this block that just captures whatever the output is from that test. And the way it works is like you can write the code and you can start with an empty expect block and then you run it and it's like this test fails. What's a test failure? It fails because the output is not equal to the thing that's captured in the test and it says oh do you here's the diff like you captured empty and like actually there's all this output and do you want to accept that and it kind of automatically like copies it in and now you have a test that passes because the output is equal to what is expected right and I just like if you look at the particular example um a fair amount of care was done to like make it relatively clear to make it easy to read what's going on and I think this is actually an important component of using expect tests. Well, if you like run, you know, some example of your program and dump a ton of output that's really hard for a human to look at, like no one will understand anything and you will have achieved nothing. Uh, but if you carefully design it so it's easy for someone to look at and read and understand the meaning and the intent behind the example, then it does something really useful. Um, you can also do like lots of different kinds of cool tests in this format. This is like maybe my favorite example of like hardware engineers really like looking at things that look like oscilloscopes.

23:15 And so plain text oscilloscopes uh for your viewing pleasure. uh the I cannot claim to like actually understand how to usefully look at one of these and understand something about like the up and down signals and exactly what's going on in in the particular but the hardware engineers swear by this stuff. They find it very useful to like dig in and understand low-level detailed behavior of a given circuit. Um and again like just having some attention to the visual presentation lets you surface you know complex system behaviors in ways that can be simple for humans to understand.

23:52 Um, another another important part of the overall approach is having the ability to kind of slice up different parts of your program and run them in a deterministic way. Um, and I think speed of feedback is a key accelerant in the programming process, right? Like as software engineers like we greatly prize the speed of the inner loop, right? The more time it takes to get feedback from a system, the less useful that feedback is for you. Um, and in this case, you can get feedback in milliseconds instead of in minutes or hours. And that really changes things, right? I mean, I think it's super important to take like heavier, more expensive testing things and like it takes, you know, 17 hours to run and if you can get it in seven minutes instead, that's way better. But getting it so it feels instant is better still. Um, and we can in this context simulate all sorts of stuff, networks, clocks, other services, all of the above. And that helps you do testing of things that are effectively distributed systems, right? You can throw multiple different programs together. And if you have nice shared abstractions around how you mock out the critical services that you're using, this just gives you a way to kind of wire them up all together and like see the systems kind of ping-ponging stuff back between uh between each other. So now you can see the value of doing this in a terminal. I can change the font size. Um, so here's like a an example that just has like a totally simple distributed system with like there's like a client and a proxy and a server and you can just like set stuff up and see. It's like oh Ant-Man like why does it take 5 seconds before my client connects? It's like, oh, it turns out like the T-Lock, which is the service discovery thing, like takes a few seconds before it like actually advertises for the first time, which is kind of a weird property. Um, and you can sort of see the interlacing of two different messages there. And like you can in a relatively small amount of code generate a view that gives you a pretty clear understanding of this slice, this trace of program behavior.

26:02 So, I just kind of want to spend a moment like defending examplebased tests. I feel like, you know, people are all very polite, but I feel like there's a certain amount of, you know, yeah, that example based test stuff, that's not that's that's the old way. That's not good. But I actually think example based tests can be unreasonably effective. Like, they sound like like expect testing in general, they sound kind of dumb. It's like I have a big complicated system and I'm going to like poke at one place in the universe of all possible configurations and look at how it works. But I think example based tests are a lot better than that makes it sound. And a key reason for it is software most software is brittle, right? When it's wrong by a little, it's wrong by a lot. And that brittleleness is actually a useful property in the context of testing. Um, obviously like the brittleleness is a is a problem. It means things fail in bad ways. Um, but it also means that it's more likely that like tests, even simple tests that capture things in a small number of places do something useful. And this brittleleness can be increased by having things that make your software effectively more rigid, right? And using types like what's great about types, it's like the power of the upside down a universal quantification.

27:19 Where are the types true? Everywhere, right? And that can the combination of like simple well-written code that leverages type systems in effective ways tends to have a kind of click in place property like you kind of you just kind of push it in the right place and like the whole thing just kind of snaps in. A large variety of things that you would want to make sure are true can be relatively effectively demonstrated by a small number of test cases. And there's real value in having a human think hard about what are the the appropriate places to like press on, right? You know, and I think that that kind of human judgment where you're understanding both the shape of the system and I actually think often the shape of the implementation. Ben made a point in the previous talk about how like you should really test against and think about your interface and I think that's mostly true but like some of the soft underbelly of our software systems has to do with weirdnesses in the implementation and I think thinking a little bit in your testing also about the implementation can help. Um, and then the other thing that it does is it adds examples that help people understand the behavior of the system, right? And I think making our systems legible to humans is just an incredibly important aspect of it. And I guess with the expect test version, you don't just get to see the example, but you get to see like behavior unrolling in the system, which is better still.

28:45 All right. And this is the problem not having a look ahead on my slides. Another another thing that I think is interesting in this is you look at the examples that people have chosen to like commit to the repo. That's not just telling you something about the behavior of the system. It's telling you something about the intent, right? Someone stopped and thought this example was worth writing down and it was an important part of the behavior of the system. And that gives you yet that gives you yet more information about what's going on.

29:13 All right. So, how does this all work in the world of agents? Um so again I think expect tests let you see the behavior uh the behavior of the system and they let you see changes to that behavior and the same is true of the agents right the the the whole expect test framework is a way of closing the loop. If you talk to people who are thinking about building good agent harnesses, closing all the loops is an important part of it, right?

29:40 You want to make the agents do be able to do as much of the process as makes sense for them to do. And expect tests are just another kind of loop closing. They give you another way at poking at the behavior of the system and understanding what's going on internally. Um, and I think when you do this, uh, where you kind of have this like low-level library-based, you know, virtualization, it gives you the ability to kind of expose this behavior and see it at multiple different scales at multiple different levels of the system. Um, and nicely it persists over time as your program evolves. They get committed to the repo and they stick around there.

30:18 Um, and surfacing things in text is really nice, right? Because, you know, it's true that models are these days are multimodal, but they're not like awesome at being multimodal. They're like the the the vision components are often missing a lot. And so surfacing things to text is a kind of very kind of cognitively friendly thing to do for agents. Um, and again, I think human understanding is really important in all of this. And the other things that expect tests do is it makes it easier for you as the person who's thinking about what to do with this change generated by an agent. Makes it easier for you to understand the shape of that change. Um, and again, you can see the behavior of the system, not just the code that was written. Um, and I think a kind of less obvious but really valuable part of the kind of overall approach here is the way that it interacts with code review. So, this goes back to like a kind of great thing about uh Excel.

31:16 Maybe you're not expecting me to say nice things about Excel, but like Excel is like a great programming system. Uh, I I have like many times, especially earlier in my career at Chain Street, kind of had my had my ass handed to me by like people using spreadsheets and like getting things done faster and being more effective at like understanding and debugging the stuff that they were building than I was able to to in like the ordinary programs in the nice fancy programming language I was using. And I think a lot of what makes Excel great is it's kind of the duel to ordinary programming, right?

31:48 When you write an ordinary program, most of the time you have this kind of very compact representation of the logic, right? The logic of the code is right there in front of you. It's easy to look at and see and understand. Um, and it's really hard to see the behavior and the flow of data in the system, right? And spreadsheets are the reverse, right? If you think about a spreadsheet, the logic of a spreadsheet is like smeared all over the system in the kind of cells there. And the way that you got the program to be set up right is that you very carefully like stretch and cut and paste and take advantage of like the auto incrementing behavior of like Excel's way of filling in stuff. Um, which you know you could get it right when you do it and then if later someone like typos something and now it's wrong, it can be really hard to notice. So that part's bad. But the good part is the data is visible and there and always available. And when you want to understand like how a given thing worked, it's easy to kind of trace back in the graph and understand its behavior. And this the kind of expect test idiom gives you something of the best of both of those properties, right?

32:55 You you both you can still see the compact representation of the logic, but you can also see this kind of more unrolled behavioral view of the system. And then when you get back the diff from an agent or from a human for that matter, you get to read both the change to the logic and then the induced change to the traces of the program that you're running. And that's just like a very powerful way of increasing your ability to understand the thing that has been done.

33:23 And then you know the final point as of all of this is like iteration time is really important. And so having an approach that gives you really high performance in the execution of these tests is really important again for the humans and for the agents in similar ways and the library level simulations enable that. All right, code review. Uh I feel like you know there was a talk earlier like yesterday about like the end of code review. Um let's talk about code review before it's all over. Uh fun party while it lasts.

33:58 Um so first of all like what is code review for? Like why do we have code review in these engineering organizations that we build? Um I think when I started at Jane Street I had a understandably narrow view of what code review was for. It was like oh this whole trading enterprise seems kind of scary. We should make sure we don't lose bundles and bundles of money by doing something dumb in a tight loop. So it was like the focus was mostly about correctness. But I think code review is about a lot more than correctness. For sure, it catches bugs, but it also spreads best practices like the way in which people learn to understand both what they should be doing when they're writing code and also what other people have been doing. The way you kind of learn about the details of how the systems are being built is through people reading each other's code. I think it's a very powerful effect. Um I think that teaching effect also increases the bus factor of your organization. Does everybody know what the bus factor is? Right? number of people who once they are run over by a bus, nobody knows how the damn system works, right? You want that not to be one for almost anything that matters.

35:00 And again, having people routinely read each other's code is a way of increasing knowledge and understanding across the organization. It also keeps things simple, right? If you just have the assumption that you need to write a feature that someone else has to understand before they approve, like that's just going to change the code that you write. and simple code has lots of advantages. Um, and indeed I think in general the the overall view of like optimizing for readers instead of writers of the code changes tons of things about the software that you build and the organization that you have like the resulting code is simpler, more flexible, more maintainable, less buggy.

35:40 Right? I think that just this is just a thing that kind of falls out of code that can be reasonably read. Um it's also I think uh more resistance to being to having your like productivity crushed by the cross terms right I think you know the experience of like starting in an organization with 35 people and ending up in one with 3,500 people like as the complexity and scope of your systems grow there are just more interactions more ways in which like the overall complexity of the system different parts influence each other and if you're not careful like your per person productivity is just going to get crushed over time as they have to spend more and more time thinking about the weird edges. And the more you can make your code simple and understandable and friendly to readers, the more resistant you are to that kind of stuff.

36:30 And then finally, it's just like a source of like happiness and joy in the work. Like operating in a codebase that was designed not just to get something done, but to be read is just a very different experience as a software engineer. And I think like, you know, I think of this as like one of the ways that we try and like keep great people is by making the actual technical work like more delightful. And I think having a kind of tight code base is an important part of that.

36:58 [snorts] So how does this work in the context of agents? Does any of this matter with agents anymore? Um, and I think it really does, right? I think one of the points to keep in mind is that agents work better in the context of a codebase that is well tended and well put together and relatively simple and tightly engineered. There's a great stunt that Anthropic did uh a few months back where they like harnessed a bunch of agents together and had them write a C compiler. Um and you know there are lots of complaints that one can that people have made about this particular experiment. I actually just think it was a great experiment and a great stunt. Um they did not produce like the next like LLVM or something like you would not want to use this compiler. It has all sorts of gaps. For example, no type system, right? It is nice to get feedback when your program is illyped like even your C program but like there was none of that. uh it was very limited in like it could compile the whole Linux kernel but like lots of other programs it wouldn't work on but it was still like a very impressive uh kind of thing to have created in this just by like you know tossing a bunch of agents at it.

38:08 Um, but I think actually the most instructive thing about that experiment is how it ended, which is to say there were it at the point it ended, there were still lots of things that were wrong about the compiler, lots of things to be improved, but they kind of turned it off because what had happened was as the agents kept on doing more and more work. They stopped being able to make forward progress because every time they made a change, they were more likely to break something. And at some point, like you just couldn't make any further progress at that point. And I think this is like indicative of what happens to agentic systems when you put them in very messy, very ugly code bases. Um, and and this like a general fact about the agents and really about how the agents are are trained is like they super want to win the video game, right?

38:55 They are trained to win the video game. Like there's a red light and they are desperate to turn it green because they have been trained over and over to try and turn that red light green. Um, and they're quite good at it. like they will do what you asked mostly, right? They will do they will do something that looks a lot like what you asked. Um um but they are not good at keeping other things going well, right? There's all these like nonfunctional properties of our code bases that we like the functional properties of what it does.

39:25 Those are really important and then there's non-functional properties of like how simple and flexible and extensible is this codebase, right? you know how how many footg guns have we left lying around? How many like repeated bits of code that shouldn't be repeated and hard-coded constants and whatever, right? And the more of that there is, the harder it is for the agent to work. So, it depends on these non-functional properties, but they suck at preserving them, right? They are just not good at maintaining the quality of a codebase. Um, and I think that makes review actually more important than ever, at least at the current horizon. Like I want to express a certain amount of humility about like what the future is going to bring in agents. Like maybe you know maybe there will be no form of like human cognitive work that has any value at all because the agents will be better at all of it. And then like you know we probably won't be spending much time thinking about our involvement in software engineering. But I think in the world that we're in now, it's arguable that code review is maybe like the most important thing that a human can do in the context of software engineering is sitting down and understanding systems and helping making sure that they're doing the right thing. And not just doing the right thing, but doing the thing in a good way.

40:40 Another just general point to make at all this is like reviewing code that comes from agents is actually surprisingly hard for a bunch of reasons. Um, one thing that we've noticed is that agents break the kind of social contract around code review. Um, this is a quote from one of our engineers. Uh, and it kind of reflects the idea that like in the old world when someone gave you code review, they had invested in it, right? And someone's like dropped a feature in your lap. It's like, oh, I should really prioritize reviewing this and getting it into production because someone thought it was worth the time to think hard about this and get this thing done. And like if you know, all they did was like, you know, point at an agent and say, could you fix this thing? And they just kind of yoloed it and hand it over to the to the person who's actually responsible for the system. It's like that's not super helpful. So there's a kind of social contract issue that this puts a lot of pressure on. Another thing that I think just makes it kind of emotionally hard is like the agent doesn't learn anything in the process like or rather it seems to kind of you know you know it does some stuff you tell it why it's wrong and like it improves a little bit in that context but then the session is over and like all is forgiven and forgotten. It's like that's like not super motivating for like at least doing the ordinary things that we do when we work with agents which is very different from what you do with people. With people you are coaching and helping and trying to improve them. Um, but that doesn't quite make sense in the same way. I mean, to be clear, you can like work on skills and improve documents and there are other ways that are more persistent, but just the ordinary back and forth of working with an agent feels very different. Um, also I think a lot of people just find it hard to like really pay attention to AI generated code review. Like there's just like a difference in the social feeling that you have when you're working with a person versus when you are reading over a thing generated by a machine. Uh so this quote you know when reviewing AI generated code I noticed myself checking out finding hard to focus eyes glazing over you know this is I think a pretty common feeling that people have and I think it makes it harder to do the level of review that I think is extremely necessary in the current world given the current state of the technology.

42:48 Um another thing that I think contributes to the above is the tendency of the agents to reward hack. This goes back to the like they're all desperately trying to win the video game and it just means that like the shape of the errors that you get is pretty different. Like you get you know just like the classic example of like please make sure all the tests pass and like some you know deletes the tests. You're like h so like you you have to look for a different set of things. You need a different set of instincts when reading over the code and like all the telltale signs you get of bad code. It's like those smells aren't there anymore, right? It's sort of like, you know, you look at like English pros and you know, people, you know, if you have a piece of pros that was like very carefully done and like is grammatically very clear, like that's some kind of signal. And like in the world of LLM, there's like no signal at all. Like an LLM never makes a grammar mistake, right? But that doesn't mean the thing it's writing is good or correct. And so this kind of disjunction, this sort of rather separation of the usual signals of quality from the actual quality of the underlying artifact makes review a bunch harder. Um, all right.

43:54 It's not all bad though, right? The agents are also, I think, can be very helpful in uh making review better. Um, maybe the main thing which has been mentioned by a number of other people is that it makes it cheaper to make a lot of the quality improvements that you want to make to the codebase to make it better over time. Um, and you people are just kind of more willing in the context of this work to ask for big improvements and big changes to improve the level of the code. Um, I think the the agents also have more direct ways to make review easier. They can do things like taking a big feature you have and breaking it into a stack of features where each individual piece is easier to understand. Again, a kind of refactoring that can be hard to ask for in practice when you everyone's trying to get things done. Having them write clarifying tests is often very useful. Also, just like using them as a kind of oracle to talk about the code, to ask questions about it. They all, you know, they'll lie to you a little. They won't give you all the right answers, but but you can often quickly sharpen your understanding of the code by talking with an agent. And I find myself doing that a lot more. And it by the time I want to go and talk to a human about it, I'm better informed and the conversation is like higher signal and higher value for everyone involved because I've like had the opportunity to before that have a bit of a dialogue with the agent first. And another cool thing that we've done a little bit of experimentation on is you can point an agent and a feature and say, "Hey, can you like design a walkthrough of the feature of like just show me here's an order in which you'd show the diffs and tell me a little bit about each one." and it can just reduce the cognitive load on the person reading the code to have this kind of guided presentation and the agents like do a decent job of doing that.

45:33 All right, so I now want to talk about like something that's not just like more of the same, right? I I I spent a bunch of time talking about all like the practices that we have done for many years that we think of as really important. I want to talk about some ways in which agents have changed our minds or are starting to change our minds about how we want to approach building reliable software. Um, and like I spend a lot of time uh going and talking to people outside of Jane Street. I've gone to lots of like nice functional programming conferences, visiting people on campus, and I've had to spend a lot of time disappointing people and saying, "No, I'm so yeah, we like fancy type systems and nice programming languages, but we're like super duper not interested in formal methods, right? We just don't want them." Um, and like that's starting to change. Our view on that is starting to evolve. Um and the thing that feels different now is our understanding of the cost of formal verification and like also how it fits into the kind of benefits that you need in the context of this kind of agentic world. So just to like for the moment like talk about how expensive is formal verification and process. So a great example is 4 which is a cool uh kind of micro kernel style operating system that was built in a very carefully formally verified way. Um it's like 8,700 lines of C. It took about 25 person years to achieve. Um a lot of that work was not just writing the thing itself, right? Not just writing the pro like some of that was writing the actual operating system.

47:03 Some of it was writing the proof. There was a lot of also writing of tools and stuff to support the formalization effort. Um they've said like ah maybe it only need 10 years if they did it again. But just kind of going to the original numbers like 23 23 lines of proof for every line of CC code and a half a person day like that's just grotesqually expensive right it's not worth it except for a very small number of artifacts for which you need extraordinarily high assurance right this is just like not the way that we're going to build all the software that we need um but it sort of feels like things are changing right where the cost structure looks like it's not as extreme as it used to be. Um, one thing is you see a bunch of increasingly impressive results in the realm of pure mathematics. So there's a bunch of really cool benchmarks uh on fairly hard problems. Not like you know no one's no one's winning a Fields medal with these yet, but like a bunch of cool, you know, you see them like hill climbing like IMO and Putnham problems pretty effectively.

48:03 Um, and there are really tantalizing results coming from working researchers, right? people like Terry Tao like getting real value by pairing with an agent while he's trying to work on formal proofs in lean. Um I think a thing that's worth noting here that I think is a really important aspect of this is it's not necessarily that the agents themselves are like so super smart. The thing I think that's really enabling at least at the current level of the technology is the agents kind of bring together many different kinds of expertise and like the agent is not as good at math as Terry Tao is and like kind of no one on the planet is um and and they're not as good at math as the vast majority of professional engine uh professional mathematicians maybe you know any of them um but they're way better at lean right and I think this is actually like a kind of thing that people often undervalue in the agents like the agents students aren't that smart, but they have memorized the internet, right? And being just kind of smart and having memorized the internet is really powerful. And I think being able to like pair I know a lot about math and I know a lot about the domain and also I have like a super smart stenographer that can like take the things I tell it and convert it into lean. It's kind of this you can like marry these different specializations together and like things become possible that were otherwise previously hard. And like I don't know you see this in this kind of very formal context. You see similar things in like you know product designers who can now like have serviceable code that they can kind of generate and build prototypes. It's a similar kind of marrying of different specializations that I think is a very powerful thing about what we can get out of modern AI tooling. And I this all makes me more excited about formal verification. There's a lot I want to see about what we can do in this space.

49:49 Um, but I I do think this is a bet. Like it is not clear to me that this will work out and I think the current level of the models don't really seem strong enough to do all the things that I hope might be possible in the space, but you know, they only seem to be getting better and there's a lot of exciting possibilities there. So, it seems to us like this is like an exciting time to potentially invest more in formal methods as a technique. So, there's a bunch of directions we're thinking about. Um just to like go through a few of them quickly for people who are interested in the space. There's like refinement types is a kind of classic way of like extending like more precise annotations in an existing programming language. I think the b our basic view on these have been like super nice to read super bad to write and if you can have the writing being done by the LLM well maybe that's enough to make the whole thing work. Um differential verification is also an interesting idea. The notion that you could like I don't know how to specify this system but I can tell you that this diff is a noop respect with respect to the following properties is like potentially very powerful. Um and you can also think about doing full proofs of correctness right like we can like spin up rock or lean or whatever and try and prove all the way down from a spec to the final implementation. Maybe the user can write a really simple, easy to reason about, maybe purely functional implementation of the thing they want and then the agent can do refining and write a much more complicated imperative implementation and show that the two are equivalent. There's like a lot of interesting space here. And then there's a lot of interesting interactions with the design of the language itself, right? Like we're doing all of this stuff in our own super weird version of OKL. Uh there are choices that you can make on the language level. Like so Varys is an interesting prover that works very well with Rust. It avoids a lot of complexities around a thing called separation logic that I don't even pretend to understand but is apparently like harder to use than other proof techniques but is kind of the thing that you need for verifying fully imperative programs. But the fact that you have this kind of ownership discipline in Rust that eliminates most forms of sharing means that you don't need separation logic and you can do simpler things and so you get sort of more juice out of that work. So anyway, these are some of the directions. We're like actually just starting to think about this. I think, you know, I feel like we kind of turn to each other and we're like, "Oh, maybe we should do this like eight weeks ago." So, it's like all very fresh. Um, but we're really excited like we're we're planning on building a team. We want to like hire people, we think, to like start a formal methods effort here. Um, and so you I don't know people who are excited, we'd love we'd love to hear from you both on ideas and people who would like to do this kind of work. Um, as just like a last point about all of this, I want to say that like when I think about all of this like how do we leverage agents, I think of it in a very personentoriented way. I've heard like people talk about like our goal should be that like people don't write or read any code and stuff. It's like it's a weird goal. Like I'm like I feel like our goals should be about trying to make people as effective as they possibly can be, right? I think these are amazing productivity tools and we want to drive human achievement and productivity and I think again there's the super weird world where like no human cognitive effort of any kind is useful anymore and like I don't even know what to do in that world but in the world we have now and I think the world we're going to see in the coming years the precious resource remains human attention right what what can people do how can they add to the process and as such we should be thinking about maximizing people's individual leverage what they can do what they can achieve and and like the the building of tools should and the building of development processes should be focused around that and part of that is making the agents more effective and I think there's a lot of discussion about how do you make agents more effective and all these kind of discussions of like feedback mechanisms and all of that I think fits into that story but I also think an important part of this is maximizing human understanding making it easier for people to understand what the systems are doing and I think this is a kind of unspoken about part of the problem and I think agents can help with that but you know there's other things that we can do as well. Um anyway this is like all part of like how Jane Street thinks about software engineering and you know we care a lot about like you know what humans can can contribute to it and we are always looking for other great people to join in. So I don't know if if this all sounds like a kind of pleasant philosophy for how to think about software engineering like you should reach out.

54:18 All right. Thank you very much. [applause] >> Sure. >> Yeah, this is a good question actually. So the question is like how do we feel about automation of code review? Um and I think automation of code review is like a misunderstanding of of the concept. Um like the fact like we have code like this we are building processes where you like have an agent write a feature and then you have a series of other agents like read over for particular things to try and improve the quality of the code.

55:12 But in some I think you should just think of this as like an accident of like harness engineering that you need to do this like maybe the model maybe like you know claude 7.3 or something will come out and then they won't need that kind of thing and they'll just be able to like generate code as good as they would and the extra level of another round of review doesn't help and whatever and like in some you think of like there's like the there's the things that the agents can do and I think code review at least the way I think about it is about human understanding. It's like how do you get to the point of the human understanding what's going on in the code? So all of which is to say I'm super pro the thing that people call AI code review. I think it's incredibly helpful. It's also super good when you want to do like oh there's these horrible practices we've had all over our tree and like I can do an automated audit and find all the cases everywhere.

55:58 It's amazing. But I I think it's really a distinct thing from the process of driving human understanding of what's happening in the system. And so I just like try to keep those think think of those as separate concepts. [snorts] >> So I uh making illegal states unrepresentable is super exciting and with with how many states you can make illegal and I think a lot of functional programmers get very excited as like look at how much mileage you get out of this technique. But inevitably you run out of gas at some point and you end up with some property that you can't enforce using system. I think a lot of functional programmers think we just need a more powerful system. mean dependent types are something that will allow us to get you know enforce more correctness types. Do you do you think that's the right path? You know I noticed you didn't mention dependent types. What do you think about types?

56:49 >> Right. So there's like old me and new me. I think I think old me is a kind of dependent type skeptic. I think of dependent types as just like another variant on this kind of formal method stuff and I mostly think of it as like not having a great kind of trade-off in terms of like the cost and complexity and messiness of using the system versus the benefits that you get. And I don't know, you look at the papers people publish. Oh, we did this great proof on like the correctness of this like balanced binary tree thing and it's like boy that is not where my bugs are, right? Like we can test that thing within an inch of its life and that testing works pretty well and like that's not where I need the help. I do however think in having richer type systems can be valuable but I think you need to take real care with the ergonomics making sure they are efficient that like you get good feedback that you get good error messages like one of the one of the uh additions that we've had that's had the most impact is we added this notion of a general notion what's called a mode which like an extra kind of property you can tag on a value and then a particular mode that's maybe like a relatively easy one to understand is what's called the local mode and a value that's marked as local is guaranteed from there forward to follow a stack discipline. And that's useful because it allows you to do type- safe stack allocation and that's why we wanted it in the first place. But it actually lets you do a lot of other things too. You can do like capability style access control where you have like a value that represents the ability to do something and you can like give it to a function and you know when that function returns it won't have stashed a copy of the capability because it can't because it's local. Um and like one small example in our Bonsai web framework there's a kind of phase separation where there's like a part where you are building kind of the overall graph of the kind of structure of the web app that you've built maybe like as a small note every web application framework is like secretly an incremental computing and state management system right because like that's what you need to build UIs and there it's useful in these kind of systems to have a kind of static graph of the computation so there's like a graph building phase And then afterwards like all the code that runs during the execution of your program and it's really easy to kind of screw it up and like do things in the wrong phase and so we just have like a capability that represents the ability to like change the graph and like you now have a marker in the type system that clearly cleanly separates the phases and you can't make the mistake anymore. So I do think there's lots that we can do by engineering the language to give us more and better guarantees. But I do think like type systems are a kind of sweet spot and when you kind of go off from like type systems to like things that look more like theorem provers, you lose a lot. Now new me is like well true but maybe agents change the calculus in the ways I was talking about before. So I'm like newly more interested in dependent types and refinement types and all of these kinds of systems in a way that's like totally might not work but I think is like interesting and and worth investing in.

59:46 Uh do we have the time? >> Yeah. Okay. So my question is on the formal methods. Uh you have shown self for there's also like cedar, there's concert and I think all of these like very big formal verification examples have this uh distinct like notion which is formal verifiability like the the requirement to do formal verification actually guides the development. it constraints it in some ways and like comfort is slower than its counterparts.

60:18 Uh I think self is also slower than its counterparts. Cedar was specifically engineered and designed in a way that could be verified. So we have to do like we have to put some constraints on the things that we are building in order to be able to verify them. Does that change the calculus uh in your view on what we can formally verify versus test? So I guess a big picture thing I think about all of this is the world in which formal methods wins is the world in which this accel accelerates us where we can get more done and do more things and you know achieve better software than we do today rather than ones where it like you know it constrains and slows us down and I think that's you know it's you know the the there was like a graph earlier about like you know the kind of trade-off between speed and quality and like it's just valid to pick many points on that horizon. And the thing I'm excited about about formal methods is that it may be the case that this allows us to kind of make appro improvements like across that graph in ways that are, you know, they basically leverage, you know, cheap and, you know, you can turn on the faucet and get formal verification. Um, it's not clear whether it works. I mean, I think the basic point of it's super hard to verify a program that wasn't designed to be verified is like true is true for many reasons. I think of like one of the biggest ones is like the program that was defined to be not designed to be verified is probably not correct. So it's hard to prove things that are false. Um and so the idea that you you know almost always we're going to have to like fix up programs to prove them correct because they had bugs in them that you're going to have to resolve along the proving process. I do think it seems quite likely to me that many of the kind of good ways of doing this will do like will have like the thing that happens under the hood be like correct by construction processes. So the idea that like I write a pretty simple inefficient implementation of a data structure that like represents my intent and then agent goes in and like develops a fast version along with a proof of the correctness of that is potentially very good. And I think that's a context where like you will get a thing that is faster than you would have gotten before because you know you've given it lean in one hand and pf in the other and like off it goes to try and make this thing as fast as it can. And you know, maybe you could have done it too, but like it was a lot of work and it wasn't worth your time. Or maybe you couldn't have done it because you're an expert in some things, but not a really good performance engineer. And again, this kind of mixture of expertises where like everyone gets to have their own performance and proof engineer like come and help them do the part of their program where they need that. Like it's that kind of thing that can extend people's individual power that I'm most excited about.

63:00 >> That question. >> Yeah. Yeah. Um I was curious whether if you picked that um style both for pros and also code um perhaps has like a unexpectedly large impact on uh ging the attention of human uh like whether you're thinking about like should documentation like have this particular touch so that the reader is and stays engaged. Um I don't know if you're like thinking about this frequently or if you Yeah, I think it's so I feel quite differently about code and pros.

63:39 Although in some ways like I don't know I think both of them are tools for thought and you know I feel like I sharpen my understanding of things both by writing English text and by writing programs. Um, but at least in a professional context, my goals around the code that's written is for it to feel kind of neutral and in a kind of shared idiom rather than like it's not great when you go into code is like, "Oh yeah, Alice wrote that and like Jim wrote that part and like I could just look at it and know by like how they chose the identifiers and whatever."

64:08 Like I I think we've really tried to build a world where the code feels like neutral and sharable and part of that is like it just like helps people do new things, right? like if you can like you know I wrote a big codebase but I wrote it in a style that's widely understood so like I can then go do something else like when something else and someone else can come in and work in that code and this kind of flexibility that you give to people to like sample from the tons of interesting problems that like we have in front of us I think is like a great thing and it requires a certain amount of subversion like submer submerging of like some like individual idiosyncratic style and like there's some sadness to that but I'm kind of okay with that trade-off whereas writing like no I think of writing like you know lots of expository and like you know writing where you're trying to convince someone of something is like a kind of very personal thing where I think personal style still really matters and kind of engaging people and and and getting people's attention and just like I don't know it's part of the part of the thing you're doing. I talked before about like the social contract of code review. I think it's like a social contract of writing when you like put out like LLM written writing. It's like is there really a person on the other side who even understood what is said here? And like I think it really I don't know there's something kind of undermining about that kind of social connection there. So like I think there's lots of good uses of LLMs to help people in writing but at the end of the day I really want the stuff I read to be written by people and not not by an LLM. Um, and and anyway, so and and one other point as a technical matter, a thing that I was worried about early and I'm no longer worried about is the idea that like we do all this work to try and build a good house style that makes it easy for someone to walk into a new codebase and understand it. And it's like, are the LM's going to write in some like super weird other style and it's going to be hard? And like it turns out they're like super good at pattern matching and they like look at the code around them and they pick up on the cues and they do a pretty good job of mimicking what's around them. sometimes too much. Sometimes they go into like a bad part of the codebase and mimic the bad stuff and like that's not ideal. But overall, I'm glad that they do a good job of like having their code feel like it fits in relatively seamlessly with the stuff around them.

66:14 >> Thank you very much, Ron. [applause]