Short answer: David Petrou says models, harnesses and possibly programming languages will co-evolve. Continua finds formal verification like TLA+ useful at concurrency and API seams, and he imagines languages that merge code with its formal specification.
Watch this answer from Episode 51 (starts at 23:29) · Episode 51 notes and transcript
From Episode 51: It Ships While You Sleep. The AI Agent OS a Former Google Engineer Built After Leaving Google., starting at 23:29.
David Petrou [23:28]: And in that case, it really comes down to the harness. Right? How are you managing memory? How are you decomposing large problems into subtasks? And so I think it's gonna be quite interesting, the coevolution of large language models along with the harness. And what we might see from certain labs is actual development of new programming languages that are intended for agents. And that could open up a number of new efficiencies, especially when you think about program verification.
Jordan Metzner [24:00]: Okay. I don't wanna get too deep into it, but new programming languages for agents to speak with. Just one quick, I guess, question there. Why would the English language or even maybe a semantic language that already exists for programming not be good enough for what we have today?
David Petrou [24:21]: We should not assume any of the ergonomics, that currently exist are is the optimal set of things for agents. I mean, if you think about, say, Kubernetes, people talk about, okay. Was Kubernetes invented or discovered? Right? So it works well for humans. It's not necessarily the right abstraction or an agent to manage, processes that that run-in the cloud. When it comes to programming, what I've found what we found at Continua is that using formal verification like TLA+ and a bunch of other ones, they're really useful if you do so at particular seams. For example, places where there could be a number of there could be a higher chance of concurrency bugs, API seams, when clients talk to servers. So in these various places where you have a bunch of state machines, it's really great to talk about what's the preconditions, what's the post conditions. Right now, something like a Go program and your formal statement of what it's supposed to do, these are separate things.
David Petrou [25:34]: So you could imagine programming languages that bring those two closer together, which would be kind of difficult for a human to deal with, but not so hard for an agent. Now whether you can single shot it or you need to fine tune the LLM, that's a whole separate story. But I would say, just to get back to my primary point, the coevolution of the model along with the harness and potentially programming languages, I think, is really where this is going, and we can't just look at some of these existing benchmarks that have already been around and are kind of showing their age right now.
Jordan Metzner [26:11]: Oh, that's a an amazing and unique perspective and obviously comes from probably some of years of experience. Okay. Well, this was a pretty awesome episode. David, thanks for joining us. How can people get ahold of you?
David Petrou [26:25]: You can find me on Twitter, d p e t r o u. I'm also on LinkedIn, and you could just go to wheelie.dev and get yourself on the wait list.
Jordan Metzner [26:35]: Awesome. Thanks so much. Thanks, Sam. Great episode.
Sam Nadler [26:37]: Thanks, Joy, and thanks, David. See everyone next week.
Jordan Metzner [26:40]: See you.
