Ep. #92, Confidence Is the New Bottleneck with Ray Myers

Ken Rimple: So Ray, you've been working at OpenHands, which is an open source agent, right?

Ray Myers: Yeah, that's correct. I would still describe it as the leading open source coding agent by a few measures, but when it started it was kind of the premier open source coding agent that was actually kind of feature complete. And now the ecosystem has grown.

As I see it, the mission of there being open source coding agents, it's so successful that you got a lot of neat options to choose from now. But yeah, when I got started and that was my motivation, it was just kind of in doubt whether that was even going to be a thing, whether they would be competitive.

Jessica "Jess" Kerr: And would you say they're obviously competitive now?

Ray: That the open source options are competitive with the proprietary ones? That is absolutely true of coding agents, yes, benchmarking any metric you look at. If we're going to talk about models which are a component of agents, then it's a little bit of a different story how competitive the open weight models are to the proprietary ones month to month. That's kind of a different question.

Jess: Right, right. So you can use proprietary models with open source agents and you can use-- No, I guess you can't use your own models with proprietary coding agents?

Ray: Well, that depends. That's kind of a product choice. But what is usually the case is they will want to be in control of which models you use. If they are, you know, a model lab themselves, like Anthropic or OpenAI, then you're using their agents, you're using their models. There are some proprietary coding agents I think that mix in open weight agents. So I don't want to draw a gross generalization.

Ken: But also one of the things you can do with OpenHands and other open source coding agents is if the person has sufficient hardware at their disposal, they can run local LLMs too. Right? So do you find that a lot of the people using OpenHands are using big GPUs on their computers and running things locally more because they want that full control over where their data moves back and forth and, and just to have it run locally?

Ray: That is one of the personas that's interested in the product. I found that the open source element comes into play much more even than I expected at the enterprise level as well. Because enterprises like control. Oftentimes they may be doing some local hosting as you kind of describe it now, or they might be using some offering that allows them to host a bigger model within their walls.

But one way or another, they like an open source offering because they are going to have control long term. Like they can run their thing their way.

Jess: Okay. And then when you have an agent and possibly a model, but even if it's an agent using proprietary models, that you're running, then you also have the opportunity potentially to know what the heck it's doing.

Ray: Good segue.

Jess: Haha!

Ken: So, yeah, let's talk a little bit about instrumentation and observability.

Jess: How do you know what it's doing?

Ken: Yeah, how do you know?

Ray: So let's zone it down to a simpler question, right? Because you might not want to know everything that it's doing. You're very motivated to know if it's failing. Like, are my agents failing?

Jess: Oh, and how do you even define failing in an agent?

Ray: Okay, so that is the right question to ask. I will say the answer to the first question is yes, it's failing. Like, if you want to know--

Jess: Haha! Is it failing? Yes, every day, just like me.

Ray:

If you want to know if your system's failing, it is. Modern websites in general are never in a state of all the way up or all the way down.

Right? They're always--

Jess: I would argue that there's such a thing as all the way down.

Ray: Oh hopefully not.

Jess: That the only way to not fail is to just not run.

Ray: They are usually operating in some-- I should have said "almost."

Jess: Okay, okay. Haha.

Ray: Modern websites in general are almost always in some state of degradation between all the way down and all the way up. Like uptime is kind of an outdated term once you have more than one server, even arguably.

Now on top of that, I'm not going to say that agents are just that same situation. They are desirable specifically because they do unexpected things. They can improvise and react to a degree of ambiguity. So they are kind of inherently a more chaotic element. But you can already be sure your website at any scale is in some degree of failure.

And your agents definitely are because they're inherently a little more unpredictable, kind of by design. And also, you know, they are a new technology that you are maybe new to using. So all sorts of reasons to be suspicious of failure. The question is, does it pass your tolerance levels?

Jess: Like good enough?

Ray: Yeah.

Jess: Does it have enough up-ness? Haha.

Ray: Does it have enough up-ness? I literally, you know, we haven't talked about this but I've been in SRE for quite a while and site reliability engineering, platform engineering kind of roles before I got involved in AI. indeed that was probably my motivation to get involved in it.

And I would sometimes say like, look, what I do is I try to increase the amount of site uppedness in my environment. So it's exactly, great, exactly what you said. And so I study the conditions that lead to site uppedness and I try to--

Jess: Haha!

Ken: You know, I have a theory. I think it's really, you could just basically have an AI picture, the "Is it fine?" dog with a fire. It's the distance of the dog to the fire and the size of the fire that are two dimensions you're looking at.

Jess: And like what's on fire?

Ray: I like this. We may have to workshop that later. So you know, to stop dancing around the question with kind of philosophizing here, are your agents failing past your point of tolerance? This is now a very business domain question. So before you even introduce anything AI specific to that, exactly what you started by asking, Jessica, like what is failure to you? Not what is it according to what the AI company thinks.

Like in your environment, what would failure look like and how much of it can you tolerate and how can you mitigate the impact? So the good news and maybe the bad news for you is I'm going to say turn around and look at your business domain, look at your context and start there.

Set targets around that, usually in the format of service level objectives, SLOs, is a good kind of body of knowledge of how to approach that. And this is all kind of conventional reliability stuff. Once you have figured out what you're willing to tolerate, then the way to measure those specific outcomes get a lot more obvious. You know, once you, once you've modeled it.

Jess: Okay, so we started talking about coding agents.

Ray: Mhm.

Jess: Then we have the generic domain of software development.

Ray: Mhm.

Jess: How can we define failure for coding agents?

Ray: Yeah, so I think going again to look at the domain and you know, so you can kind of carbon copy what I'm about to do. Whether you're talking about a coding agent or an agent that you know, books flights or, you know, which is I think kind of a strange thing for one to do. But they seem to like it in the ads.

Jess: Haha!

Ken: Going to Alaska to go 30 miles. Yeah, yeah.

Ray: Or you know it, it helps you troubleshoot alerts or whatever it's doing in your environment. I'm always going to say like look at the domain. What does failure look like in the domain?

I think that failure in software development might look like someone involved in the situation isn't getting what they want out of it, which is often either users are not happy because the end code is buggy or doesn't do something they want it to do, or maybe product owners are unhappy that they can't ship fast enough.

It is sort of all these things that we wanted out of software development is to get a lot of value for everyone involved.

Jess: So outcomes, we're looking at outcomes of buggy code, of unreliable code that has degraded its uppedness of insufficient features or not meeting the expectations.

Ken: Some of that is quality not only just definable by a number, but your developers are working in the IDE, they're calling the coding agent. They're seeing that it's not answering the questions the way they want to. It's taking long path around something that's not just simply a number.

Jess: It's leaving a bunch of comments that the next agent is like, "oh well where's Kafka here?"

Ken: Boy, that sounds familiar.

Jess: Oh, we took Kafka out. Oh, but it put that in the comments all over the place. No Kafka, no Kafka, no Kafka. Guess what that agent is thinking about? Oh, sorry, that was this morning. Haha!

Ken: So user feedback is one of those quality level judgments that a human has to enter. That goes into it too, almost like with let's say an evaluation or something like that.

Jess: All of those outcome failures are lagging indicators. Right? This is after the code has gone into production or at least into some sort of evaluation test kind of testing. Can we detect failure earlier?

Ray: Yeah, absolutely. So there are, as you know, like well trodden philosophies of shifting left. You know if we figure out what failure looks like when it's actually doing damage, you know, how can we catch that earlier and earlier and earlier?

And a lot of the work that's gone into making coding agents more consistently valuable has followed that line. It's like, how do we catch failures earlier and earlier and earlier? There's something kind of unique, about them in that there is this agent loop that is sometimes going for many steps in between a human looking at it.

So, you know, shift left can kind of go even further. If you can get shift left all the way into the agent loop, then you know, that is very convenient if your signal is good. Right? Because it can be finding and fixing the issues before they've resulted in you shouting, why are you babbling about Kafka? Or whatever, you know. Ha!

Jess: So this is like when the agent can tell immediately by running its own tests, or whichever verification process, that it's screwed up.

Ray: Yeah. If you shift left far enough, you know. So you could imagine in the metric land, you've got leading versus lagging indicators. Shift left is going toward leading indicators. So I'm saying abstract terms like "shift left." But, you know, many people will talk about, okay, we need code standards, we need linting, we need type checking, we need various things that allow us to get assurances earlier in the process.

These are some things that are, that are thrown around. But it's important to just look at your situation of what's holding you back, not to just open up a book of best practices and implement them in random order.

Jess: It's way too early to have best practices with agents. We have tips and tricks.

Ray: Yeah. So this is where I would push back on that slightly.

Jess: Great.

Ray: And say that you can have best practices within your domain that you recognize are still relevant or still maybe need only a little bit of tweaking to be--

Jess: Okay, so, tried and true best practices for software development applied to agents?

Ray: Yeah, yeah.

Because ultimately, what we're trying to do is do the task well. And we're not starting from zero on what success looks like in that domain. Regardless of whether you're trying to use AI to make software development or transportation or education better, we have bodies of knowledge on all this. And the reason I am so keen on saying this is because there's this AI first mentality that has gotten to the point of actually actively throwing away what we already know about doing this well, and then just hitting a wall and needing to rediscover it.

So, you know, I'm trying to help you steer clear of that.

Jess: Do you have an example on either side?

Ray: So one of the new terms that has come out with using coding agents has been called loop engineering. So this is just in the last couple of months we started saying loop engineering. We were saying harness engineering and context engineering before that.

And, you know, I see these less as new techniques that are coming out, but as like the communication strategy is evolving. Like, a lot of the thrash you're hearing is, okay, we think we found a better way to communicate about how to be successful. It's less actually that new components and techniques exist under the hood. But, we do need to iterate on how we communicate to users. So.

Jess: Okay, so it's not that loop engineering is super different from context engineering or outcome engineering, but let's think about it this way.

Ray: I am contending it's a framing. Yeah. So pretty much you talk to anyone who is knee deep in agents the year before that, they're going to say, well, this is obvious, but I don't want to trivialize it because communication is important.

Jess: Nice.

Ray: But if you look at loop engineering, it seems to present as some big epiphany that you need to think about the whole software development life cycle.

Ken: Yeah, I think we figured that out a long time ago that you need a life cycle and to follow one.

Jess: For some definitions of weak.

Ken: I mean, many times, many times over, many different definitions. But so I think of loop engineering part, I think of, for example, Claude, there's the Ralph Wiggum loop. Is that what you're talking about is like figuring out specific steps that are taken in each kind of loop of set of changes or things through the system. Right?

Ray: So I initially thought loop engineering was about the Ralph Wiggum loop. And they had just like found a better name for it, which would be good. Like, I don't think we can call it Ralph Wiggum indefinitely.

Jess: Haha!

Ken: I know. There was another one I saw just the other day too. Claude Superpowers is another one I'm thinking of like that.

Ray: Yeah.

Ken: Where it builds TDD into the loop and breaks things apart into multiple agents and attacks each feature that you're going to take on as a separate agent, et cetera.

Ray: Yeah, it's not exactly that, but, I'm not really the person to tell you this is what loop engineering is, because I am precisely saying that is a repackaging of stuff we already had names for.

Ken: Yeah.

Ray: So then you take what would Old Guard versions of this knowledge look like? Well, continuous delivery. There's a website called Minimum CD where they're like, you know, this is our attempt at making an official definition of continuous delivery so people can stop thinking it means build servers or something.

And they have a selection of practices and they've even like updated them. "This is what agentic continuous delivery looks like." If you look at the literature from people who are, you know, AI forward companies trying to teach you how to use it well at scale, they will either by name or just by like component, be talking about the practices of continuous delivery that made that work.

Jess: And that's quick, accurate feedback. Right? As soon as you can get it?

Ray: That is a huge part of it. Yeah.

Jess: Charity Majors talks about and has stickers about the human on the loop. We are in control of the loop. And the loop here is that agent turn from "I'm trying to do stuff" to "I think it works." All of that stuff that happens before it comes back to you and says, okay, I'm absolutely right. Haha.

Ray: Yeah. So you want something to happen along the way saying you are not in fact absolutely right, you know, before it gets back to you--

Jess: If you're not.

Ray: Yeah, yeah. And the better, you know-- So a lot of meta work then is going into how do we make it come back with my expectations. And everyone would like, the users would like people to just ship agents that do that out of the box.

But it turns out the work is very contextual and if you want to be like a heavy adopter, you're going to have to do some of that platformish work of how do I get the right signals into agents? You're going to have to lift the hood.

Jess: And we talked about the signals. What it needs to know is, is the software buggy? So that implies good test suites and does it meet expectations, which requires good requirements or behavioral specs?

Ray: Yeah. So we are basically thinking about how our intent travels through the system. How will it get from some sort of product design to an implementation or a change to an existing one more likely. And then as we implement, how do we know our assumptions throughout that are carrying forward into what's actually at runtime?

And we have lots of ways like tests and types and design conventions, even architecture patterns, all sorts of ways that we have discovered of making it easier to maintain intent throughout the cycle. So we just want to make sure the agent is respecting how our chain of intent works. And in some cases we're enhancing what our engineering practices are going to be that convey that. But I see this as very much the same game we're playing.

Jess: Chain of intent.

Ray: Mhm.

Jess: Say more about that and some of the practices that we can use to keep it intact.

Ray: Yeah. So you hear people talk a lot about intention lately and I think that's because there's like a gulf. There's kind of a void of intention that has been created.

Jess: A void of intention?

Ray: Yeah.

Jess: That sounds frightening.

Ray: Like, I think we were all-- Obviously you were always trying to make software do what you want, but you have to make these concepts very first class, if that is threatened.

Jess: Like what you want needs to be first class or--

Ray: Your intention.

Jess: Like a particular intention.

Ken: Because sometimes it's just up here. As an engineer, right. You're sitting there, you're coding. If you're doing it, the intentions in your wetware, in your brain, it's not expressed well enough to the agent in many cases. Right? L ike getting out in the first place and then carry it along through the loop?

Ray: Yeah. So you might say like write down the requirements and another way we could say that is you need to externalize your intention.

Jess: Yes.

Ray: You know, and this is also ways that we communicate to each other and so on. T here's in fact usually more than one user of a coding agent involved in the situation. So we find a lot of things that worked before, like writing stuff down and showing it to each other, you know, is also allowing an agent to go more healthily.

There's a kind of a family of practices called spec driven development that you've probably heard or maybe used that-- I think this is not one specific thing because any time anyone tries to criticize it, someone says like, well actually you could do it a different way, but I think it is generally speaking helpful and also completely rediscovered.

Again, we're like spec driven development is just sort of a family of techniques for writing down your intent onto usually a markdown document so that the agent will have something to consistently refer to.

Of course, we also have a lot of history in not only doing that, but making the spec executable in various ways as tests and other ways.

Ken: Yeah.

Jess: Right. The spec can be executable with like behavior tests. And I know at least one of my friends, Steve Ko, will not let the agent change the behavior tests. That's a hook without explicit permission. But there's even more rigorous ways to express intent through formal verification?

Ray: Yeah, I mean you can get as rigorous as you like. And I kind of contend that we should. But when I use the word should, I should put a context around it. Right? Because some people will say, and we shouldn't call complete unmitigated shenanigans on it--

Some people will say that just writing stuff down is enough now, like I just put stuff in markdown and the agent does it. I don't even need to think too hard about like what his dev process is. And like I deliver value and it just works. And then you're like, okay, well what are you doing?

And it's like, well I'm, you know, maybe I'm, I'm selling T-shirts and I'm a team of one and whatever. You know, like there are even commercially viable applications of software that don't rise to a level that can meaningfully be called software engineering. Right? And are nonetheless valuable. Right?

Like Excel is the most widely deployed programming language in the world. Right. And like there's a few layers above that that just are not at a size, complexity and risk class that like a lot of the things I spend my career focusing on are going to be that appealing.

So to the people who say like vibe coding's enough, have fun with that. I'm working on stuff that doesn't apply to a lot of the time.

Jess: Yeah. If your software is used by many other people's software, that depends on it, and breaking that contract has consequences throughout a whole industry or your entire customer base, that's different.

Ray: Yeah. So as we are injecting, you know, new forms of risk with also some compelling upsides with AI development, I start to look at well, what do we do at the highest gross scenarios already, what techniques exist? I first dove back into automated refactoring.

The sort of things we can do in a JetBrains editor with the right click menus and like I can do an extract method and a rename and extract class and so on with like near zero possibility that I've broken something. So this source of safely changing code became very interesting to me.

Jess: Yay. Type systems.

Ray: Yeah, type systems. And also syntax transformations. But both of these things help us refactor with confidence. In addition to tests--

Jess: Confidence, there's something we're after.

Ray: Yeah. We want confidence that our intent has been preserved. Right?

Ken: And also it doesn't drift over time. Right? So we're talking about this chain of intent. Right?

So if you've spelled out what you need and what you want it to turn into. And you have this, this is my intent. As you're going through all the steps and you get to the point where you're generating tests and running tests and verifying the tests work and then running through the system and booting and all that stuff, you see that things start to drift a bit, I would think that's also part of building an agent is to detect whether the agent is going off the rails and not following a plan the right way, not actually executing what you're asking for in the right amount of steps reasonably for what you're looking at. Right?

Jess: Earlier, Ken, you said Claude, the king of workarounds. Haha.

Ken: Yes. I'm just going to paper over this and it's still going to be there in a commented block of code. Thanks. And then Codex said, what are you doing? You know, this should be-- Like, thanks other agent, for my agent that told me my other agent wasn't doing the work.

Jess: Haha.

Ken: Oh, before we go any further, Ray, can we ask you who you are?

Ray: Yeah, I'm Ray Myers. I'm currently involved in an effort called The Coding Agency to improve outcomes in software through public literacy and better tools. I have been a professional software engineer for 20 years, been a tech lead in four different industries, and most recently before this, I was chief architect of OpenHands, an open source coding agent.

Jess: Great. Okay. So we were on preserving chains of intent.

Ray: Yeah. So I recognized that I really liked it when I had ways, some scope of activity in which the agent would never break anything, like if I made it only act through syntax transforms. But it's a limited number of people that want to only do safe refactors of code and don't ever actually want to do a behavior change.

So I kind of looked, okay, what else do we have? And this is where I kind of rediscovered this active field of computer science called formal methods. Right? And so a lot of programmers are familiar, for instance, with a quote by Dykstra that says tests can show that bugs are present, but never show that they're absent.

And they assume, usually, what he's saying is that you can never know bugs are absent. But actually, you know, because Dijkstra was a capital C computer scientist, what he meant actually was you can know bugs are absent, but you have to use math.

And you know, we as programmers, kind of deny our relationship to math, our status as amateur applied mathematicians. But, you know, one way to say what formal methods is, is trying to apply mathematical rigor in how we reason about programs and use other Programs to help us do that.

Ken: At the simplest level isn't this things like cyclomatic complexity and like code coverage at a bare minimum there's like percentages to apply. Right? Say hey, you only have 10% code coverage when you're testing and that's, that's a big white line.

Jess: That's again only presence of bugs. The best you're gonna find is it's not great.

Ray: Yeah.

Jess: But proving correctness. Now it's not gonna work for all of your T-shirt website, but it might work for just the pricing calculation service.

Ray: So Ken, what you're suggesting, while it involves numbers, you know, it's very much an informal method because you know, code coverage tells us something but nothing to do with the requirements of the program.

Ken: Right.

Ray: If we're doing formal methods, usually we're targeting the actual business facing specifications. If we're selling T-shirts, maybe you would encode something like, "we can never double bill." "We can never charge someone twice for the same purchase."

Jess: Or, "we never sell one that isn't in stock." That would be unrealistic but provable in theory. Haha.

Ray: Yeah. Some people like to imagine, like to do this, we need to encode every conceivable behavior of the system and prove everything from the ground up and maybe even like go down and prove the hardware or something. While there are efforts that are almost that big in scope, really any single time you have any expectation of what the app is going to do, you have a chain of beliefs.

And we can encode that and we can help us think about it and know that we're actually doing something valid. It doesn't have to be-- I think it is actually so applicable that someday we will do this even when selling shirts on a somewhat small scale. But right now some of the big adopters are starting to be like cloud providers.

Jess: Talk about the tools that they use.

Ray: There are two main areas I'll talk about today probably. And one is formal specification, which is just proving things about your design, which is a lot more helpful than you might think. So the advantage of that is that you don't have to change what you're implementing it in. Your system can, on a technological level, you can make the same technical choices you were making before, what language and so on you use.

And then you use some special language. Like TLA is a very popular one. A new one, Quint is like that but a lot more friendly. I would recommend trying Quint and you just say hey, I've got some--Race condition is a great way to start, when we talked about double purchases and so on. Like, a lot of that's race conditions.

Model the system using Quint and tell me if its design, you know, avoids these scenarios. Then you have an additional problem of wondering, did my implementation actually match the design? That's real. But you would rather have that situation than be trying to perfectly implement a design that was already buggy. And every time I have done this, I have learned something through modeling it.

Jess: Okay, so like, our intent, this is actually, tests for our intent of does the intent as we've expressed it, actually function as we believe it would? That's pretty great. And then you can use agents to be like, hey, does this code implementation in Node match the spec I've written up in Quint?

Ray: Yeah, and I've done that with Quint, actually. And it's like, it's surprisingly successful. I think that you want to be aware of the idea of the agent not making the same choices you might make about what to model and what properties are really important to the business.

But this is surprisingly effective nonetheless. And there's formally this very manual back and forth between looking at your implementation, looking at your spec, and seeing where they might diverge, that agents are really good at that little menial stuff. There's other quality practices like mutation testing that I've also started doing more that I have agents, because it's just tedious.

Jess: What's mutation testing?

Ray: Oh, no. Okay.

Jess: Is that like, if I change this, does it really break?

Ray: Yes, yes. So if your test coverage is good. Right? So people criticize test coverage --

Jess: Because you can get great coverage by calling some code and then returning true.

Ken: Right.

Ray: Yeah. But if you did mutation testing, if you changed the behavior with like a random modification of the code, then ran the test, they would still pass. You would see that-- Okay. As they say it-- This is a weird thing they say, but in mutation sets, ah you haven't killed all the mutants.

Jess: Haha!

Ray: Killing all the mutants in mutation testing means that any random variation I could make on the code, they have like, programs that go try to screw up your code. It's kind of like chaos engineering before you deploy, right?

They try to screw up the actual code and introduce a change. And if your tests don't catch it, then it's likely that you have effectively a coverage gap. You might have complete, measured test coverage, but you haven't actually validated all the behavior.

Jess: So this is a test for your test?

Ray: Yeah, yeah. Now that's an example. So I was just making a comparison. Right? And this is a practice that I usually don't have the patience to do, but with agents I now do. Like if I ask them to do this, they can usually find some, make some good discoveries. And it's one of these things that like you can use agents in ways that strictly improve the quality.

Jess: Yeah. So in this you're adding something to the loop. So if your loop includes writing tests and then writing code, you can also add tests for coverage. Was it's just a precondition of the mutation test to test the test. And you can put all this before the agent declaring done. I think of all that stuff as scaffolding. It's like it's not the production code, but it's around the code so that you can work on it more effectively.

Ray: Sure.

Jess: And agents support building more scaffolding.

Ray: Yeah. You know, of course we can imagine a world in which you end up with too much scaffolding or a bunch of-- I've heard the phrase like rigor theater.

Jess: Like code coverage, right? Haha.

Ken: Right. Yeah, sounds like it. Yeah.

Jess: And like metrics that get reported upward about how much code coverage you have.

Ray: Yeah. So here's the thing, right.

I've changed my mind about metrics a little bit, but only because I started out like, sort of against them to a fault, like most engineers have kind of learned. But you know, I'll say this, I wouldn't want to be without metrics. And our distrust of them largely comes from believing that whoever's using them is probably not engaging in systems thinking such that they will know what interventions produce results. They are actually not using the metric to inform a reasonable mental model. And that objection is right most of the time.

So I understand it. But I would say that as metrics go, test coverage is actually like one of the best. And it's just that like all metrics have scopes in which they don't tell you certain things. And so you always need to supplement it with other data.

Ken: It's an indicator, not necessarily a symptom of the actual problem.

Jess: But now, now that it's you looking at the metrics based on what the agents do, of course the metrics are good.

Ray: Well, that's not the point at which I changed my mind, but I hear, I hear that, I hear that. Right?

Jess: Haha!

Ray: And I will say even even further. Right? A lot of people will make statements like ah, ah, now that we've got agents, all devs are managers.

Ken: Yeah, right, right.

Jess: Feels like that.

Ray: I guess if you've like never met a good manager in your life, which is a fair number.

Ken: Not all devs can be managers and not all managers can be devs. So we'll just do that.

Ray: I'll say this, if we're going to insist on turning senior devs into expensive bad managers, then like, I guess it's an improvement that we're not inflicting their lack of management skill on humans.

Jess: True. Let them manage robots.

Ray: Yeah, but I think a statement like this is like, okay, you delegate, you communicate, you do, you know, they're naming things that are things that managers do. But it's like maybe closer to you know, product management and project management than like people management and stuff.

Like I think there's just so much dilution of like what skills and outcomes are at play here.

Jess: okay, okay, okay, I'm going to come back to this bit about managers. But first I have an open loop on, you said there were two kinds of formal methods. There was formal specification. What's the other one?

Ray: Yeah, and there are more, but those are two worth talking about right now, I think. So the other one would be formal verification. Like you literally are proving properties about the implementation code and actually that is the one that fascinates me more, even though it's a lot harder to adopt. And this is the one that I think should be informing the design of programming languages going forward.

Jess: Are type systems a limited piece of formal verification?

Ray: Yes, yes, that is correct. You could think of any result from a type checker as a form of proof.

Ken: What are some of the other areas in addition to type checking that you could associate with formal verification?

Ray: Well, I mentioned that we can't have a situation, you know, maybe where you've double charged a customer. Now those temporal logic based modelers like Quint and TLA plus are very good about doing that with lots of simulation of a design. But you can also do properties like that, business facing properties, on the code itself. Right.

So it really, it's almost open ended of what you could in principle prove with enough effort. But it's a question of like, you know, what is worth your effort?

Jess: What is an example of a tool that people use for formal verification of this type?

Ray: Yeah, one that's talked about a lot right now is Lean Prover. So it's just called Lean or Lean 4 is the current version if you want to search for it without finding other uses of the word Lean.

It is the one I would recommend getting into if you want like a general purpose theorem prover and not just one of these sort of specialized model checkers, but just the deep end of the pool where everything's possible.

Lean is the one that has been able to invest the most in user experience over the last couple years. And it is sorely--

Jess: A user like us?

Ray: Yes. Yeah, like programmer, developer experience. And it is sorely needed in this area. So that is the one I would recommend. Even though it's actually like right now, more used by mathematicians than software engineers, I would still say it's got, you know, momentum and it's a good one to get into. Others are Rocq and ACL2 and Isabelle are some proof assistants.

Jess: How do you spell Rocq?

Ray: R-O-C-Q.

Jess: Obviously. Haha!

Ken: Haha! To be exactly what we found in a search engine, perhaps.

Ray: Yeah, it used to be C-O-Q which, because it's French.

Jess: But we got tired of saying "Coq" all the time?

Ray: Yes.

Jess: Reasonable. Okay. And these are all things that we can do if we want to use agents to drastically improve the quality of our code instead of just shove stuff, something out there faster.

Ray: Yes. So a broad family of tools and when I, you know, as I say, formal verification is the deep end of the pool. If you think it's like not practical for what you're doing, then, you know, you may well be right. But I think we want to ground all our meta decisions in the direction of being able to somehow verify both the correctness and other properties we need, maintainability of the code we work on.

And this is even more important now that you can kind of get as much quantity as you want as long as you can have confidence in it. Your sources of confidence are amplifying what you can accomplish to just a absurdly obvious degree. It was true before, I think, but it is now, you know, a very stark difference. When we have sort of almost as much velocity as we could care to have.

Jess: Right. We can have all the code we want, but the confidence is another thing.

Ray: Yeah.

Jess: And the more of these tools we can use to get more confidence in our code, the more we can ship. But also when the agent can use these tools as well, then it's more likely to produce us something correct on the first try. Okay. Okay.

Speaking of that loop where the agent is doing stuff and then trying to figure out if it's right and then doing a bunch of stuff, if we are going to be bad managers, or less bad managers, of these coding agents that we're operating, that gets back into looking at what the coding agents themselves are doing and like the experience that it's having.

Like, how many times does it have to go around that loop? How many circles does it get stuck in? How many rat holes does it go down because the comments are about Kafka, just because there's no Kafka?

Ray: So this is where, if you want a self contained learning path of how to get better at doing this, this is where I really like the Ralph Wiggum loop as an idea. Right? Because it teaches context management and it also teaches you to study failures. So these are good instincts generally.

Like the people that were really seasoned using these things were often doing these kinds of habits. But this is how I contrast it with just something like, okay, just use a spec, use a plan. Okay, it does involve that, but it also involves like, I'm trying to get it to run on its own and solve as much as possible without me.

But the way I'm doing that is when it fails, I'm coming back. I'm studying it. I'm studying the agent conversation. Like, oh, was it yelling about Kafka for like 50 turns, whatever? And I'm seeing, how can I set the system up better next time?

Jess: Yeah. Is that something we can measure?

Ray: Yeah, I think that other than just software outcomes, I like to have agents do incremental commits, for instance. So I think there's a lot of useful stuff there. If you don't want to look at an entire agent trajectory, which an agent can help you do. Trajectory, I should say, is another word for conversation in this context.

Jess: Really?

Ray: Yeah.

Jess: Oh, that's useful.

Ray: An agent trajectory is just like the log of the messages in the conversation. And it sometimes no longer makes sense to call it a conversation when it's talking to tools and not talking to you.

Jess: Okay.

Ken: And you can diff very quickly between them, the agent can anyway, since you've got all those little commits.

Ray: Yeah. So there are various ways of detecting when it seems to be flailing around in the course of this conversation history. And you can also look at incremental commits and you know, see, okay, where, where is it going off track? How much time, how many tokens is it spending? I talked to a testing coach recently who said they've started to rebrand their stuff as like, "instead of teaching you XP and high quality engineering, I'm teaching you token efficient engineering."

Jess: Nice.

Ray: You know, wow. So that's the thing. If it's screwing up a lot. Right? And it has some loop trying to get it to retry and fix itself. It's probably very token inefficient. But these require skills of, you know, evaluating things, which depending on your scale will change a lot how you want to evaluate them.

Jess: Right. Because you put tests into the loop so that the agent can have feedback on its work immediately. But then we put evaluations on top of the loop of how did that go?

Ray: Yeah.

Jess: Like when you talk to someone-- As a manager, when I talk to someone on my team and I'm like, how was your day?

Ray: Yeah. And so you could imagine, and this is, this is not a crazy idea at all. You can imagine like after every session ends, doing an agentic review of it to produce like, okay, we got stuck for this long, or these were the problems and so on. But you know, at the end of the day we're just talking about like, you know, good old fashioned root cause analysis and prioritizing improvement items and stuff.

Jess: Because is it old fashioned root cause analysis when you're doing evaluations?

Ray: Well, what you do based on them is-- Like in eval. We say evaluation so much. Right. In machine learning fields we have shortened it to eval is often in terms of a, okay, it got 60% or whatever. But if you're in the business of improving that, then you're going to ask a lot of follow up questions.

Jess: Yeah.

Ray: You know, actually when we adopted OpenTelemetry at OpenHands, I was involved in putting that in and I thought the app developers were going to be the first users of it. But it turned out that the agent team, the people who are like actively tuning all these little things based on like their machine learning pipelines and so on, like they were the most interested in the OpenTelemetry because they were, you know, going through agent conversations and figuring out what was happening so we could make some tweak to get our benchmark scores to be better and ultimately to be sure that those were reflective of meaningful experience.

Jess: Nice. So the agent telemetry let you measure at a high level whether there were problems and where there were. And then they had to drill into the individual conversations to investigate.

Ray: Yeah, I think if you're using metrics in a curious way, in an intellectually curious way, then you're going up and down the levels of abstraction. Right? Like, okay, this is a big picture of what's happening, but that is telling me what question I want to ask next.

And the kind of lowest level of that, if you're talking about agent behavior, is usually like reading the raw logs of, okay, what did it send to an LLM? What did it send to a tool at every little step? And you know, we do some of these that have thousands of steps in them, you know, so that's just for one conversation.

You want to know what happened in the whole conversation and across a thousand of them. You can't always be at that level of abstraction, but you've got to be able to go up and down and get a picture of what's going on.

Jess: Yes, exactly. I heard someone say the other day, zoom in to understand, zoom out to decide. Like in the details you can see kind of what's happening and then in the aggregates you can say, well, is that important enough to do anything about?

Ray: Yeah, I like that, I like that. I think that's a really good way of putting it. I will say things that are a little more esoteric to mean that, you know, different levels of abstraction and so on. You know I like the zoom in, zoom out idea.

Jess: Yeah. It is what Honeycomb is built for. So hence this podcast.

Ray: Smart people.

Jess: Haha. And it's great that you added OpenTelemetry to OpenHands, because it's something that I struggle with, with like Claude Code. I can get it to output traces now, but they don't tell me everything I want to know and they're not structured the way I want. So I have run OpenHands in the past just so that I could modify the traces to express to me what the heck is going on in this conversation, in this agent trajectory.

Ray: Yeah, that's, you know, makes you sound more like one of the researchers, I guess. Haha. Which may be a good or bad thing, you know. But yeah seasoned terms.

Jess: Great. Where can people find you online? Where can they go to learn more, how can they contact you, et cetera, et cetera.

Ray: Yeah, well, I just launched a new podcast called The Coding Agency. You can find it at thecodingagency.org and so that is I think a nice place to start for the messages I'm focusing on now, but it's brand new.

I've got a YouTube channel called Craft vs Cruft as well. That's been going for quite a while and is kind of aimed at mid career software developers looking to get better. I've been doing that for quite a while.

And you can also reach out to me directly on LinkedIn, in particular, if you like the general thrust of the coding agency and are thinking, I would really like a resource up there or an episode on this topic that I'm trying to figure out, then please do talk to me.

Jess: Great. Great. Ray Myers. That's M-Y-E-R-S. And we'll put links in the show notes. Thank you for joining us.

Ray: Yeah, thank you for having me. I'm geeked to be here. A lot of my heroes have been through here.

Jess: Cool.

Ken: It's been great.