Episode 015 · September 8, 2026 · 01:18:41

Programming Languages for AI Agents

Dan Gerlanc
Dan Gerlanc
Podcast Host
Julien Verlaguet
Julien Verlaguet
Founder and CEO, SkipLabs

Julien Verlaguet explains how SkipLabs is building Skipper, a closed-loop coding agent around an AI-tailored, reactive development environment. He and Dan Gerlanc weigh the promise of faster software work against code quality, junior-engineer training, and the limits of formal verification.

0:00 −01:18:41

Dan and Julien discuss Skipper, SkipLabs’ closed-loop coding agent. Instead of asking a person to prompt, inspect, and redirect an agent, the user supplies a specification and Skipper handles the back-and-forth internally, more like a compiler producing a working result. Breaking a spec into subpieces is standard. Julien says the real differences are a reactive programming approach intended to limit technical debt and a development environment constrained around what AI systems handle well.

That environment starts from a reimplementation of a relatively large subset of TypeScript, preserving idiomatic TypeScript because agents already write it well. Julien defines reactive programming here using spreadsheet semantics. A program forms a graph of computations, and when data changes, only the necessary pieces are recomputed. The larger ambition is to regenerate a clean structure as requirements change, rather than repeatedly patching a codebase.

Julien posits a hypothetical large repository where every change triggers a half-hour test run, then contrasts it with incremental reachability analysis that identifies affected tests in less than a second and reruns only those in a few seconds. If a service is built around the same reactive model, he says deployment could likewise invalidate and recompute only the needed pieces instead of taking the whole service down.

Reactive programming also changes what the developer has to model. Where Buck or Make work around file-level artifacts and explicit dependencies, Skip’s collections can be mapped, reduced, and queried through dynamic lookups whose dependencies are tracked automatically. In Skip, the type system rejects mutable state that would break incrementality inside a map closure. Intermediate artifacts live in a file Julien compares to a SQLite database, and the computation is designed for concurrent, multicore use with multiple readers and writers.

SkipLabs began with the Skip language and looked for products where that language would provide an edge. AI redirected the company toward tooling, where incremental computation reduces the latency of the loops agents need.

Julien likes the language-design work more in an LLM world because experiments can test whether a type-system change helps code generation without navigating as much subjective human feedback. Still, he misses the other side of language design, where choosing a notation can help people understand a problem.

Julien’s own workflow is deliberately multi-agent. When coding, he keeps four, five, or six agents on different tasks, works on one diff himself, gives feedback, and interrupts when an agent makes a dangerous design choice. He still uses Emacs for text and for small but subtle refactors where supplying enough context to an LLM is more trouble than doing the work. He says most refactorings go smoothly, but generated tests still need careful review because they can be plentiful and useless.

Julien doesn’t think AI can quite replace engineers just yet. He has not seen an LLM that can design something like Postgres or the Linux kernel, rather than reproduce a known implementation, and he says current models are far from that level of taste. They can remove grunt work, but they also make it harder for junior engineers to learn through small tasks, production failures, and debugging. He thinks schools and pet projects should preserve some programming by hand, even as senior engineers gain more from tools they know how to judge.

On formal methods, Julien is enthusiastic about the connection between specifications, proofs, and programs through Curry-Howard, drawing on his experience with Coq and model checking. He sees the strongest fit where semantics are stable, such as an older language, kernel, or compiler.

For evolving software, a good specification can be harder to write and read than the program, and a small API change can trigger weeks of proof maintenance. The closing outlook is cautious. The next year or two may be a bumpy road as skills shift, but after the dust settles, software engineers may spend more time on difficult, interesting design work.

When it comes to replacing engineers, I yet have to see a model that is capable of designing something large and tastefully.

We don’t do things because they’re easy, but we do things because we thought they were gonna be easy.

As long as we’re in a world where we cannot trust LLMs, they cannot possibly replace jobs.

I think for learning, we should keep programming by hand.

Skipper
Closed-loop coding agent built by SkipLabs.
SkipLabs
Company behind Skipper and the Skip language.
Skip
Reactive programming language created by Julien.
Hack
Meta-developed language Julien helped design for large-scale code.
reactive programming
Spreadsheet-style change propagation and dependency tracking paradigm.
incremental computation
Dependency tracking that narrows recompilation, testing, and runtime work.
Buck
Meta-associated build system used as a comparison.
SQLite
Single-file database used as an analogy for artifact storage.
Coq
Proof assistant Julien used before its Rocq renaming.
Rocq
Current name of the Coq proof assistant Julien mentions.
Lean
Theorem prover mentioned alongside Coq and formal methods.
Curry-Howard correspondence
Types and proofs connection underlying verified programs.
formal methods
Mathematical techniques for specifying and verifying programs.
model checking
Verification technique Julien practiced alongside proof assistants.
Emacs
Text editor retained for manual work and difficult refactors.
Bun
Project used to illustrate a Rust rewrite.
Transcript

What does the job of programming language designer look like when agents are writing most of the code? In this episode, our guest, who led development of the hack language at Meta, and I will discuss the consequences of designing for agents as the principal consumers of a language and development environment.

Welcome to Agents and Engineers. I’m your host, Dan Gerlanc. Today’s guest is Julian Verlaguet. Julian is the founder and CEO of SkipLabs, the company building Skipper, a closed-loop coding agent. He created Skip, a reactive programming language, and led the design of Hack, the language Meta developed to run its code base at scale. In this episode, we discuss.

How Julian refocused SkipLabs towards AI, what it would take for AI to be able to fully replace software engineers, and the use of formal methods with LLMs and AI agents. Enjoy the show.

Julien, great to have you on today. Thanks for joining us.
Thank you for having me. very I’m thrilled to be here.
So tell me a little bit about what you’re working on at SkipLabs.

yeah, so I mean we can talk about the specific product, which is Skipper. So close closed loop coding agent basically means a coding agent that works like a compiler more than you would work with coding agent. So a typical coding agent today is something you interact with, right? You have a project, you let it go, build things, and then it gets back to you, ask questions, and then you there’s some back and forth, right? And then you converge on whatever you you’re trying to build.

A closed loop coding agent works more like a compiler. So you have a spec, and then you give that spec to the coding agent and say, all right, spit something out that works. And all the back and forth that would have gone between me and you know the the the agent happens within itself. and so I think well that’s the product. what’s interesting about the way we’ve built the product is how

Is

well what’s interesting is what we needed to build to make this product. so we’ve built a development environment that is really tailored for AI. And so among the interesting things that we’ve built is our own version of TypeScript. So it’s a re-implementation of TypeScript. it’s a subset, but it’s a relatively large subset. and it supports very idiomatic TypeScript because agents are good at writing TypeScript and we wanted

To make sure that agents could use code that they’re used to. And with that, we use that as a basis to go build an entire ecosystem that was perfectly tailored for agents. I can get into more details, but for example, agents, LLMs are very different in the kind of things that they get stuck on. So if you look at a human being, typically a human being will get stuck on.

things that require too much context, right? So for example, you have a C++ template, from back in the days, let’s say before Clang era, like you have this this stack of thing, because the C++ template is just something that unfolds, right? It’s it’s it’s a glorified macro. So the C++ people would hate me for this. But more or less what’s going on is you’re specializing and specializing and specializing and you you hit a point where you hit a typing error.

And now back in the days, all you would get was, you know, a huge stack, a huge stack of things, and very, very difficult to follow for a human being. That’s typical, typically the kind of thing that’s not going to be hard for an LLM. You you give it a ton of context, you give the whole context, and if the window is large enough, which it will be, it will understand where where it was at and will understand the error. however, sometimes they struggle with other class of errors where humans

don’t. And so it’s it has been interesting this back and forth that we’ve been going on that we’ve been going through trying to tailor something for for an AI. Super super interesting work.

So then in terms of the closed loop, how does the when you start with a spec, I guess how is that different from what a lot of folks are doing for spec driven development? Like there’s frameworks out of AWS, like superpowers, Jesse Vincent’s framework. I guess how does your approach to doing that

Differ or compare.

So

that there’s so there’s the part where you take the spec and you break it into subpieces, and that’s really standard. There’s really no with the black magic there. That’s pretty much what everybody else is doing. I think the two things that we’re doing differently is one, because we have used reactive programming approach, we claim, so that claim still has to be measured properly, but we want at least to

Produce less technical debt when things have to evolve. and the second angle is we have created this development environment to keep the LLM in a very constrained environment. So these are the two, I would say, novelties. So I already spoke a little bit about the development environment. I can talk a little bit about the reactive programming aspect. So first, what is reactive programming? And if you ask.

You know, four people in a room, you’ll get five different opinions. So it’s one of these things where it’s like functional programming. No, nobody really agrees on what it means. and so reactive programming in in our case, what we mean by that is react reactive in the sense of spreadsheet semantics, right? Where you have a program, so you can think of it as a spreadsheet, right? You have a program, this program has different pieces of data.

this these data they were computed using some kind of data flow, right? Some kind of formula, right? And when something changes in the graph of computation, you only recompute the pieces that are necessary. So that’s what I mean by reactive. To some people, reactive means streaming. We can have endless debates about that, but you know, that’s what I mean about it. So now imagine you have structured a harness and an agent.

that is structured this way. They’re structured like a graph of computation that is supposed to produce an output. Now, when the user wants to make a change, things change a lot compared to an existing stack because in an existing stack you’re going to take the existing code base and you’re gonna patch it, right? And the risk that you’re gonna that you’re gonna have if you keep on doing that over and over again is that you you’re going to accumulate technical debt. And

You know, after a couple of months of iteration, you have a Frankenstein of a code base that nobody understands. So our bet is that if you use reactive programming techniques, basically the goal is to output a program that would have been the program you would have outputted had you started from scratch, right? And so this way keep the technical debts to a minimum. so these are the two two things that we work on.

And both are I think are novel. But then the rest is very standard, you know, taking the problem, splitting it up into smaller pieces. I mean, nothing new under the sun there.

So how does the reactive paradigm allow you to build the build a program or code base that would be more similar to if you had engineered it, I guess, by traditional means or what you’d started from, I guess h how do you create, I guess, metrics around that or
Yeah, that’s the part where I mean we’re still very early on in that and I don’t claim to have great benchmarks. this it’s still aspirational at this point, but that’s that’s what we’re working on.

And when you started SkipLabs, is you had created the Skip language originally. Is did you think were you initially working on solving this problem or is this something that

as LLM’s AI became more popular that you realized, hey, this is a place where we can apply this technology and

really make a difference.

Yeah, it’s it’s it’s definitely the latter. It’s

definitely the latter. So when we started SkipLabs, the idea was we have Skip, it’s a programming language to write reactive programs. Think of it as an incremental program if you don’t like the term reactive. And we were thinking selling a language is really a bad idea. It’s it’s a bad business. so let’s try to build products where the the language give us an edge.

And so we started with other products, but then AI kicked in and we were like, well, we cannot miss this. We have to be part of of this revolution. And the obvious place to be was tooling, because the where reactive reactive computing can give you an edge in different places. So for example, if you have a server-side logic and this logic is very complex.

and involves multiple clients and you want everything to be collaborative, then a reactive server is going to be super useful because everything is going to update automatically. And so writing the logic this way makes a lot of sense. So that’s one area where you can have an impact, which is what we were more invested in before the AI, before AI really kicked in, you know, in in and changed the development world.

But the second place where reactive programming can make a huge difference is for tooling, because by making the tooling incremental, you can bring down the latency by a lot. And given that AIs want to go in a loop and want to iterate faster and faster, then if if you are able to provide tools that are efficient at scale, you are in a really good place to build a good development environment for an AI. And so that’s how we end up in that.

In that in that place.

So does the tooling you’ve built essentially provide faster memory for a repo or means of caching what the agents already know? Because I mean, every time you start an agent, you’re starting from scratch. You have to discover anything that you haven’t put into the context already.

So

it’s not so much about what the LLM knows, although there are things that you know can be done like writing down notes and things of the sort, but we are not the only ones doing that. I’m more thinking, let’s say, you know, you have tests and you have a large code base and you realize that every time you make a change, you have to rerun the tests.

And that’s taking you half an hour because it’s a large code base. And that means that every time the LLM wants to iterate, well, it’s going to be long, right? So now that’s company A. Company A has a code base, they use an LLM. Every time the LLM wants to do something, at least half an hour. So now imagine Company B, you have a development environment where you’ve written an incremental reachability analysis, which means that every time you make a change.

You can instantly know which tests are affected by this change. And now you get that’s that within, you know, let’s say less than a second. And then let’s say only four tests are affected. You just rerun that. You went from half an hour to, you know, a couple of seconds. Now, Company B has a huge advantage because if it keeps on iterating like that, it will outpace the companies that.

So what I mean by low latency tools is what I is what I mean there. And I don’t mean so man so much tricks with, you know, the context and what the LLM itself can do, more like the development environment itself.

Got it. So in terms of compil like compilation or type checking or running tests, you have the whole dependency graph built in here so you can do the minimum amount of work per iteration, essentially.

Yeah,

and you can also do that at runtime. So if you teach the AI how to build a reactive program using the framework that we’ve built, you can also you’re not forced to take down your service. Let’s say you have a service, right? This service is running in production, which means that it has caches, it has all sorts of data, and it takes time to load this service, right? Well, if you teach the AI about reactive programming, the deployment phase itself doesn’t have to be

doesn’t have to be an all of nothing thing. So it can be, you know, you invalidate the few places that need to be invalidated and and recompute that. So there’s the phase, the compilation phase, everything that’s static, but also at runtime, there are, if if not all, at least some parts that would make sense to build this way.

And is this all natively built into the language and IDE development environment versus like if you were using a workflow tool like Buck was I guess the one I think that Meta released where you have to explicitly model the dependency graph, things like that.

So there is a development framework that’s built for Skip the language itself, but then we also ported the framework to JavaScript. So we have a version that works for TypeScript. And what you’re going to get is something less efficient because there is some overhead in running in JavaScript. But the principles are the same.

But what you’re describing when you’re describing Buck is actually pretty different from what reactive programming looks like. So maybe I can just give you an idea of let’s say you were building a tool, and I’m going to give you an idea of what it means to build a reactive tool like that. So let’s say your tool is something that I don’t know parses a bunch of JSON files, and then within within those JSON files.

goes figure out, you know, some kind of relationship between two objects. There’s some some sort of join, you know, it’s taking some data here, some data there, and then dumps, you know, generate some code. All right. Let’s say that’s the tool, right? So typically you’re going to if this was something built with buck or a make file or anything like that, the granularity has to be file-based, right? you have to create artifacts in every single

Intermediate artifact is going to be a file. And there are many cases where this is not ideal. The cases where this is not ideal is when you have to do lookups, right? I have an intermediate value that was produced. I need to dynamically look up names within those values, so I don’t know what I depend on. So writing that down is going to be very complicated using one of those tools, right? So if

You need to

model it explicitly. You you need to say what the dependencies are, which is a lot

Yeah. Yeah. Exactly.
of work.

Exactly. So here this is how it would work. The idea is you forget that you’re writing anything incremental. The incrementality is completely transparent for you. The only thing that we ask from you is that you use primitives that we’ve given you, and those primitives are there for your own good. Because those primitives are there to make you split up the work into independent pieces as much as possible.

So for example, what we don’t want is you are iterating over files and without realizing it, you are incrementing a counter internally, right? But if you’re doing that, this is bad news for you because now if one of those files changes, one of those files is is is inserted, all the count for all the other files change and you you just you you just broke incrementality. So we give you.

one construction, which is the most important one. There are others, but the first one is map. So let’s say the first one is we give you a construction where given a directory, we’re gonna give you a set, a collection of files, right? And so the collection is really the the the bread and butter of the reactive computation. You’re gonna get collections and your goal is going to manipulate those collections to create more collections, right?

So your first collection is a collection of files which contain file names, which in this case, what you’re going to do is you’re going to map over them. Map when you map over them, you’re going to use a closure. And that closure, if you are in skip, it will be guaranteed to be safe. Meaning, if you try to close over something mutable in that closure, we will not allow it. Or if you try to modify a global, we will not allow it. So basically

There there’s mutation allowed in the language, but the kind of mutation that could make you introduce state in the map is not going to be allowed. And that’s going to be transparent. The type check system is going to tell you. So you do your first phase, and the first phase you’re probably going to parse the JSON. So now you have a collection of parsed JSONs, right? Then you do maybe two separate maps, one where you extract one piece of the information that you needed, where then another one where you do another.

Then you do a reduce and you get the final result. Every time you had to do lookup, you could do lookup. So it’s not a map reduce where when you’re using Hadoop or these kind of schemes, you cannot access the elements in the collection. You always have to do a map. This is not the case here. A collection, you can actually look up elements in a collection, right? So the map is what’s going to drive the computation, but it’s not for every single lookup, you don’t need to do a map.

Basically, you can look look things up directly. Every time you look up something, all of that is tracked for you. We know what you looked up, and we will take that. So now you have your tool, you compile it, you run it for the first time over your JSON files. We’re going to ask you to give us a file where you want to put the artifacts. So what we’re going to do is we’re going start the program. It’s going to run over the JSON files and all the things the

Intermediate artifacts that we need to keep for the incremental computation are going to be stored in this file. You can think of it a bit like a SQLite database, you know, where SQLite stores the artifacts in a file. And then this file is now going to be your source of truth, which means that if you restart, you know, not the source of truth, sorry, it’s the the place where we store the artifact. Now you restart the computation.

It’s going to go through the files, stat them, figure out which ones have changed, but it’s going to use the ones that you stored to s to start the cache, invalidate the right things, recompute the right things, put the file back into a good place. Right. And all of that is concurrent and multicore. So you can have multiple people using the same file at the same time. This is all, you know, multiple readers, multiple writers, this all works.

So it’s it’s very different from something like Buck or a makefile, right? It’s it’s much, much more dynamic, I would say.

and inherently built into the language or or frameworks

you’re using here versus

Yeah, yeah. Exactly. Yeah.

the others versus bolted on after the fact essentially.

How does it feel today to be working in language development in the world of AI where most software programs are being written by LLMs or agents instead of people?

So I think it’s awesome for me. but I know a lot of my friends who are in the language field, they hate it. I think it’s because I I don’t like people. And so and so it’s nice for me. It was it was it was one part of the job that I never liked when designing a language was the constant whining from engineers. So I love engineers, but software engineers especially, but I have to admit that when it comes to subjective topics.

they can be they can be really difficult. And I think part of the the problem is when you work in software engineering, you used to have a machine that proves to you that you’re wrong. So you wrote this program that you had in your mind and then it doesn’t work. And you you have to basically accept the fact that you’re wrong and and you you need to figure out why, right? And so the problem with that is that the the the compiler and the runtime and a program that doesn’t work

Is such an is so absolute that whenever you’re dealing with another problem, which typically is going to be a matter of taste for a programming language, you will see behaviors that are annoying, right? Like you you’ll have the guy who comes in and tells you, Life is not worth being lived if I don’t have this feature. Yeah, come on, dude. Like just just just chill. I use a programming language every day that doesn’t have this feature and I’m good.

And so what I like with LLMs is that as as a language developer, as a language designer, you are operating with something that is way less emotional. And so there’s a lot less, you know, human in the loop. So this part I like because and when you make a change, for example, when you make a change to a type system, if you’re dealing with humans, it’s very, very long and complicated to know if this change is good because

You need to figure out if the new way of doing things is gonna go well with engineers, right? And and a lot of it is subjective, so it’s gonna be long and complicated. With LLMs, it’s super easy. You run an experiment, you know, all right, is it better? You know, does it help the LLM produce better code? And so you are back to criteria that are more objective. So that’s the good part. The not so good part is part of what I liked about designing programming languages is that it helps.

humans better understand, you know, pro problems and programs and reason about them. And I think it’s it’s a bit the same in maths, right? Like in maths, if you have, I think I don’t remember who said if you have the notations, you you solved the right notations, you solve half the half of the problem. Or something like that. I’m paraphrasing. But you get the idea. Like the right notation is also the right way of thinking about the problem. And a programming language is a bit that, right? Like if you have the right

way of writing it down, then you have a right way of structuring it in your mind. And that is yes, a little bit sad that you know there’s at least less attention on that these days because most of the code is written by LLMs.

So if you were starting your career working in languages today, do you think you would still focus on language development?

That’s

a tough one. it really depends on where LLMs are gonna land. So you have people who are telling you basically software development is dead, and you know, and we’re gonna get AGI, GIs around the corner. You even have the people who say nobody will have a job, right? And basically no company outside of Anthropic and OpenAI will be worth anything in two years from now. So okay, well that’s a possible future. If that’s the case, then no, I wouldn’t.

probably not, you know, go for programming languages. But frankly, I don’t know what I would go for. I would probably go for a job that has nothing to do with engineering. You would go for a job where machines cannot replace you. So probably something with deep human connections, something like that. Right. now let’s say this is not the future. Let’s say for the sake of the argument, for sake of argument that, you know, there’s still going to be room for programmers and LLMs are going to help, but

They cannot be trusted 100% of the time. So we still need people who think about structure and whatnot. Then I would say, absolutely, absolutely, I would go for programming languages. you know, I hear all these people say, don’t go into programming careers. I mean, there’s only one very narrow possible future where that’s a good that’s good advice. Because what’s likely to happen is that all the and which is what happened every single time there was, you know.

a revolution in in the field of engineering was all the engineers are gonna get much much more productive there will therefore be much much more money to be made because much more wealth will be produced through software and so if that’s the case then yeah I would say I mean it’s definitely gonna change. you’re not going to design a language today the same way than pre-LLMs. So it’s it’s going to have an impact, right?

But yeah, I would I would go for the same thing. Like if I believe that, you know, software engineer is still gonna be around in five five years, which I believe it will be, five, ten years, then yeah, I would go for that. No problem.

How do you think the job of software engineer will change or look like in five years at least relative to where we are today?

So yeah, I mean it’s it depends if I’m in San Francisco or not, right? Like every time I go to San Francisco, I meet with a bunch of friends. So I used to live in the Bay Area, I lived there 10 years. So every time I go back to San Francisco, I see all my friends in San Francisco, and I’m like, you know, walking out of there. Yeah, AGI is around the corner and you know, we won’t we’ll all be out of the job, out of a job in two two years. And then I go back to Europe and

Talk to a bunch of friends based here and they’re like, Yeah, these guys are nuts. This is never gonna happen. So it really depends on when you ask me. I would say n right now I’m in Barcelona, so I guess I’m more I have more European take on this. And I think LLMs are gonna change the game. They already have. But I I don’t think LLMs are going to be the all

you know, this super intelligent thing that is going to be better than every human being at basically every single human task. So the future of software software engineering I think is bright. But then again I’m I’m an optimist.

All the shitty stuff that you used to do as a software engineer you won’t have to do anymore. Right? Think about that shitty refactoring that nobody cares about.

There’s this thing, but it’s subtle enough that a tool cannot do it, right? If it was renaming a method, then the IDE can do it. But let’s say it’s a little bit more complicated than that. You need to add a parameter here, remove one there, and do these kind of things, right? Well, no need for that anymore. LLMs can do that. You just l let an LLM loose on this stuff. Another big one that was constantly an argument was migrations, right?

So, and typically with programming languages, that was often a big argument, right? Which was, well, we would use this language that is better, but the ecosystem of this other language is so much richer than is it safe? Are we gonna do that? Look at what happened with Rust rewrite, right? Like from Bun, right? So, I mean, it’s it’s he has access to the latest and greatest from Anthropic and has

infinite credits. So I’m not saying that anybody could be pulling something like that off outside of Anthropic today. But chances are high that in a couple of years anybody will will be able to do that. Right. So you have a Rust program, you’re you have a Rust ecosystem and you realize that there is this library written in Python or whatever whatever it is, chances are high you will be able to let an LLM loose on something like that and say, hey, come back to me with an implementation of this thing in Rust. Right.

And it comes back and boom, you have something. Which means that the job of software engineering is going to become much, much, much more interesting. You’re basically going to be left with the interesting problem, the hard stuff, the stuff that requires taste. You know, how do things fit together? Are they is are the core principles respected? Is is everything harmonious, if you see what I mean? The stuff that’s fun, the stuff that we want to do. Nobody I don’t want to spend.

Five

hours, you know, refactoring something, you know, that is brain dead and gives me carpal tunnel syndrome through Emacs and because I’m using the same macros all the time. Nobody wants to do that. So from my perspective, that is probably the most likely future. A future that is fun. LLMs are little assistants that go do all sorts of grunts that the grunt grunt work you don’t want to do. You focus on the fun stuff. We build

much, much more software and it’s awesome.

Do you miss coding by hand?

I do, and sometimes I still go back, even though I know that an LLM could probably do it. So right now when I code by hand is basically when it’s complicated enough and small enough that it’s not worth for me wrestling the LLM. So typically I’m at the core of the type system. I’m working on something very, very subtle that will have implications on the rest of the system.

I know the AI doesn’t have all of that, all that context. So instead of wrestling an AI, I just write the code myself. But I would say outside of those few cases, pretty much everything else I leave it to an AI these days. Yes, I am going to miss it. I’m probably going to do it for fun still, sometimes, you know, in my spare time, especially for educational purposes, which is a good segue into my next point, which is that I believe engineering schools.

should

have people programmed for a few years without an LLM. Like for for a while. Like rediscover those principles. And the the reason is you don’t understand a thing the same way when you programmed it yourself. And you understand it even better when you programmed it yourself, you’ve seen it go to production, and then the mistakes you made are coming back to haunt you.

Then that’s when you truly learn another level of understanding, which is because you know, when you do something yourself, it’s cool, but when it’s just to get a grade, once it’s out there, it doesn’t really matter anymore. You know that it’s gonna be graded and that’s it, you’re done, right? When you know it’s gonna be in prod and you’re still young, you’re dumb and hopeful, at least that’s that’s how I was. And it’s like, I’m gonna be fine and I’ll figure this out. And then you know, when you when you’re woken up at two in the morning because something broke in prod and you realize that.

Clearly you knew that this was fragile and you shouldn’t have done it this way, it changes your perspective. So I think for learning, we should keep programming by hand. I think for pet projects, when you’re having fun, you should definitely go, you know, do things by hand, especially if it’s for if it’s for educational purposes. But you know what? There could also be some kind of weird fetish come coming back. Like, you know, for watches, for example, if a watch is made by hand.

It’s worth a lot more, right? And it’s the same watch and usually it’s not as good as a watch that was put together by a machine, which makes sense, right? And yet the machine that was made by hands is worth more. I wonder if there’s something like that that just, you know, that becomes a trend. And people say this was actually written by real people. And therefore, yeah, the software is not as fast, not as good. It doesn’t ship as many features, not as often. But you know what? It was made by a human, that’s worth a premium.

Maybe I don’t know. I don’t know what what things are gonna look like. Yeah

H handmade artisanal artisanal code

made in Brooklyn.

Exactly. And you’ll see, you know, engineers in their little shop and they’ll have, you know, beautiful pictures behind them that is local made and you know, stuff like that. I don’t know. You you don’t know what’s gonna happen.
What does your workflow with agents typically look like?

so typically I have multiple LLMs working at the same time. and I go back to them on you know on different occasions. I have a ton of tooling that I have put together to help me go from one project to the next. So I have several repos and be able to share things and do that do things like that. I know there’s tooling that came out to help with this kind of stuff, but since I scaffolded my own, I haven’t taken the time to go

look at that stuff, which is wrong. I should probably take the time to do that because for example it took me forever to switch to git, which would in retrospect was stupid. I was still using SVN, you know, way, way, way past the point where I should have switched to git. And the reason is I built a bunch of tools above SVN back then that I knew well. But in retrospect, like no git branching is way better than whatever, you know, whatever I built. So I should have switched earlier on.

but anyway, right now I basically have four, five, six agents. So it depends if I’m coding, right? If I’m not in a coding phase, if I’m doing CEO stuff, then that’s a different different story. But if I’m coding, yeah, I have four or five agents. usually they’re working on different things. And then I work personally on pieces of it. I I will have one diff that I’m working on myself, for example.

And then I go back to the different agents and give feedback. Sometimes I watch them as they’re doing something. I don’t necessarily just go async all the way. especially when I know that there is probably a lot of design decisions to be made that that could be dangerous. And then I just interrupt, you know. I s I see it doing the thing that I was hoping it was not gonna do. It’s don’t do that. you go back to

go back on the right track right away. But yeah, that’s that’s what it looks like.

What do you have in your custom tooling that you think might exist differently or what have you set up for yourself that the world should know about?

It’s really not it’s not

rocket science and frankly there’s nothing the world should know about. Otherwise I would have open sourced it a long time ago. It’s really dumb stuff, like you know, being able to go check, go take stuff from another repo, integrate it into this one, you know, stuff of of this sort, which I don’t think is the right way of doing this anyway. So yeah, it’s

It’s bad. It’s like my Emacs macros. I use a lot of them. They’re all bad. I would not open source them and I would not, you know, encourage other people to use them, but they are my Emacs macros and I use them. So yeah, though frankly nothing nothing to to to talk about here.

you’re still using Emacs as much with the LLMs generating code?
A lot less. I use Emacs still because I still need to manipulate text, but it’s true that so I’m not sometimes I find myself going a little bit too far with LLMs, you know, where I’m like, ooh, this word here is misspelled. No, I mean maybe
Mm-hmm.

not that, but you you get it. Like basically getting the LLM to do something that would have been way, way faster to do with a text editor. But most of the time I don’t. I still use Emacs, but

Let’s just say that my Emacs superpowers are a lot less useful, but there are times where it still happens that I need it and sometimes it just comes out of nowhere. So I remember refactoring that happened a couple of months ago. And the refactoring was really not that complicated. So for example, so to give you context, there was a pretty-printing function, and this pretty-print printing function was pretty-printing a type

Now in that type, they could be type variables, except that the pretty-printing function would just print the type variables without the environments. And without a typing environment, you don’t know what the type variable is bound to. So you end up with an error message with a type variable name, which is not great because you don’t know what this type variable is bound to. So I wanted to improve the error message when there was a type variable, and I thought, okay, I need the typing environment.

In that function, except that this function was used in quite a few different places. So now I needed to pull in, you know, the substitution pretty much everywhere and thread at it, thread that in, right? And look, it took me forever to get the LLM did not succeed. It was a nightmare. So I was like, okay, look, I need the substitution of the typing environment in that place. Make sure you thread it. So it starts well and then

Does its thing and then it reaches the point where it’s say, well, here, you know, I don’t really have a substitution at this point. So I’m just going to give you an empty environment. And you’re like, no, no, I don’t want an I don’t want you to make up an empty typing environment. that’s going to be a horrible error message, and it’s going to be an error message that’s wrong. And yes, I understand you don’t have the typing environment there, but that’s the job. Like go figure out, you know, how to.

Get the typing environment to this point. That’s the job. That’s what I’m asking you to do. It keeps on going. And then it starts saying, I see, you know, in the diff, it started to create new pretty-printing functions. And I found it strange. I was like, why do you need new type pretty-printing functions? There’s one, it’s the only one we use. So I look deeper and it created other pretty-printing functions that did not take a typing environment.

So that in all the cases where it didn’t want to do the job, it could call these, right? And it kept on going, right? This back and forth, like do the job, do the job. And it’s it’s very rare this happens. Most refactorings, they just go flawlessly. But it’s one of the rare cases where it’s like, all right, open my Emacs, rolled up my sleeves,

all right. It’s good old, you know, 2020, back to the old days. I’m gonna do this, right?

So there are still examples where even on not so complicated things, you still battle, you know, fight with the LLM and sometimes that fight is not worth it. And then I go back to Emacs when that’s the case.

Yeah, I I don’t know if this has been your experience, but my experience has been LLMs are, of course, faster than any engineer and in some ways better at understanding some things like super cryptic error messages, but all in all, on average

the quality isn’t as good as what I would expect from a very good engineer, human engineer doing the work.

we’re very far from that. And that’s why, you know, whenever I talk to my friends in San Francisco, I mean s when usually when I arrive on the first few days, I’m looking around with all the, you know, all the ads that say AI for this, AI for that. Even in the bus there’s ads for what the AI can help you for. And when I have those conversations, I’m like, you guys are nuts. Like, I mean

You really think that this thing is gonna take our jobs in in six months to a year? Like for me, the quality of the code that is output, yeah, it’s not there. It’s really not there. Like it’s not nowhere near, you know, what a really good engineer who I trust, what what what they would produce. So I’m still excited because it can still do a lot of grunt work that I don’t want to do, so that’s cool.

But when it comes to you know replacing engineers, I I yet have to see a model that is capable of designing something large and tastefully. And then then I will say, okay, now we can talk. So for example, for me, the bar would be: let’s say you know there’s an LLM that produces, I don’t know, something like Postgres. So let’s say it was a database and you said,

I want a database with this and that property. And let’s say it was capable of producing by itself something like Postgres, even Postgres from 20 years ago. Doesn’t have to be modern Postgres, right? But let’s say a solid version of something like Postgres by itself, with these extra properties, meaning it’s not, it didn’t copy the design of something else. or a kernel.

Yeah, let’s say it’s capable of putting together a kernel that has certain properties that are not Unix, so it was clearly not copied from another kernel. That’s when I go like, wow. Wow, wow, whoa, whoa, whoa. We need to take five steps back. And if it can do this kind of design, then yeah, then I would see the job of engineer or software engineer is the days are counted, right? But what you see is very far from that. Now again, I don’t work for Anthropic.

or OpenAI for for those frontier model companies. So I don’t know what they see. Maybe they see a model that is, you know, so advanced compared to what we see and what has been released to the public. They have data I don’t have. But let’s just say with what I see today, no, I don’t think LLM right now, the ones I use, even the best ones, we’re pretty far from you know what an experienced engineer would would produce in terms of code quality.

Yeah, and I think that’s a good example, like go build Postgres without copying existing Postgres code or a specification, because even in a lot of the cases of implement C or things like that, there’s a lot of specification that’s out there already.

And they they read GCC,

they had access to all the C compilers in the world, and they used the the the C the GCC testing suite, right? And it was really shitty. Like, you know, that was put together as an example that they were proud of, saying, Look, it built a C compiler. It was a really bad C compiler. If it if I had been one of my students, this would have gotten a D or something like that. It doesn’t compile half of the no not half, but it doesn’t compile the examples and then

The way it compiles things is really, really naive. So this is a good example of I’m looking at it. So I’m impressed because clearly that’s something that we were not capable of doing, you know, a couple of years ago. So it’s still impressive in itself. But to deduce that, you know, we are around the corner of something that’s going to just replace us all, I I think it’s a stretch, but there are people who I respect a lot and who I think are

really, really, really smart people who disagree with me on this. So, you know, God knows who where where we’ll end up.

Yeah, I think it’s it’s hard to say because a year ago I wouldn’t have been using LLMs to write code or trusted in a loop on a code base. So are we gonna hit the same inflection point differently in a year? I don’t know. I can’t it’s it’s kind of hard to say.

But usually with the technology, what happens is that there’s a point of diminishing return. And I mean, I do understand that, you know, LLM so far, the more data you’ve thrown at it, the more the better they’ve become, and the more compute you’ve thrown at it, the better they have become too. But it looks like it’s slowing down, right? Like at least in terms of we are we are getting to a point where in terms of costs for companies who are using an LLM, does it make sense to pay, you know?

the latest and greatest, it’s questionable, you know. So I think we we are either at the point or close to the point to diminishing of diminishing return. And so you know with every technology, you usually underestimate and then usually overestimate overestimate. That’s that’s usually how I go about things. You first underestimate because you’re this new thing, yeah.

And then you’re impressed with what you see, and then you think that it’s gonna change everything. And and if you look at every revolution in the past, we’ve always overshoot with everything. You know, when it was building trains, the infrastructure, you know, there was a lot of speculation and and there was a bubble. Then it was the same with electricity, and then it was the same with the internet, and now it’s with LLMs, right? Like we

I wouldn’t be surprised if we went a bit far on this one. And and if there is a correction. Now it doesn’t mean that it’s it’s gonna be useless or over or the it’s still gonna be super interesting, right? There was still a Silicon Valley after the dot-com bubble burst. But and I think if there is a bubble, because I’m not a specialist, I I don’t know, and it bursts, it’s still going to be interesting. But I think it’s human nature to first underestimate.

You know, I give you something new and you go to, I’m not interested. I want to use the stuff that I’m used to. And then once you realize that there is something new, then let your imagination go loose and this changes everything and and and go too far.

How have you found being a CEO in a world where you have LLMs in terms of running, structuring a company?

It’s complicated. It’s complicated because they change everything all the time. It’s also complicated in terms of financing. things have changed a lot. and it’s you know, every three months things change and things change pretty dramatically. so it’s it’s very difficult. I wish the company had been built a little bit later.

And we could have started within the LLM, you know, ecosystem directly, rather than having to adjust, because that’s always more difficult for a company. But I think it we’re not it’s not too bad for us. we I still find it super exciting because you know, building tools and programming languages in a time where every tool in every programming language has to be reinvented.

It’s pretty cool. It’s pretty exciting too, you know. So yeah, there’s there’s silver lining, you know, it’s not perfect, but there’s some interesting stuff that’s going on.

Do you think LLMs let you focus on more of the things that interest or energize you because you can outsource or automate more things that would have required more of your time before?

Yeah, definitely. now I will put a caveat here, which is that

Sometimes you have bad surprises. So, I mean, let’s take one one example, right? Let’s say tests, right? And you’re going to save a bunch of time by writing a bunch of tests, having a LLM write a bunch of tests. But reviewing tests is not fun. And that’s something normally you would you didn’t have to do in the past. In the past, whenever one of your colleagues was writing tests, you would check that the test

made sense you would check also that the coworker did not omit something blatantly you know wrong something something was blatantly missing but you were not carefully reviewing tests right this is not a a job right now with LLMs when it comes to testing I mean they’re fast at producing those tests and they’ve gotten better it’s a lot better than a few months ago.

But they still have a tendency to write tests that are completely useless and just completely miss the point of you know what testing should do, right? Which is that really capture all the problems before they occur. So do I gain time? Yes, I’ve gained time, but it’s not perfect. Now I need to spend time actually reviewing carefully tests, which is a job I didn’t have to do before, right? So it’s not.

It’s not as good yet as I as I wish it was. I wish I could just say go write tests and it just works. But it’s better than it used to be.

Do you think if you were working in an area that was less technically demanding in some way or required less of a fine layer of abstraction that the LLMs would do a better job?
I don’t know. I don’t think so. I don’t think so. I think basically coders are probably those who are going to benefit the most from LLMs. So it depends when we mean LLM or AI, right? So if we mean AI in general,
AI.

then AI in general it can do a lot. Like so I mean look at what did for protein folding, right? If for this kind of stuff

It can change the game completely. And it will probably change the game for many, many, many professions, especially in science, I think in maths. it can do a lot for mathematicians because mathematicians they have this thing where the computer can actually check that the proof is correct, which we cannot do with with a program, at least with not typical programs. And

And so mathematicians they probably have more opportunities for an AI to help to do, especially the proofs they don’t want to do, they don’t want to find particularly interesting, they just want to know if the result is true or not. Now, for LLMs, I think there’s a I don’t know that they’re going to bring all that much outside of coding because you cannot trust them, right? So

I mean, yeah, sure. If you have a job that involves a lot of words, it’s gonna help you. Like you are a lawyer and you don’t want to read that 300 page document of, you know, another case related to yours. Yeah, it’s gonna be super nice to say, hey, ChatGPT you know, make me a summary of this thing. Explain to me how it’s related to this case, right? That’s gonna be good for that. It’s gonna help with, you know, jobs that involve manipulating words, right?

But as long as we’re in a world where we cannot trust LLMs, they cannot possibly replace jobs, right? Because if you cannot trust them, you need somebody with judgment to, you know, make sure that the LLM is is is doing the right thing. And

The trick that consists in saying, okay, we’ll have one person using their judgment to do to judge the work of five other people, that could be cognitive overload, right? Like let’s take, you know, the the example of a lawyer again. Can a lawyer follow five, six, seven, ten cases at the same time and be able to have good judgment on all those cases? And I say ten because I don’t know what I’m talking about. Maybe, you know, it’s fifty. I I don’t know how many cases they they usually

deal with. But you know, if let’s say it’s 10, can they do 50? Because now they have an LLM that helps them go faster? I don’t know. They still have to build context on all those cases. They still need to understand, you know, the ins and outs. They still need to understand the trade-offs. The fact that they can go faster in some cases, I don’t know that this allows them to, you know, that this allows them to just fire the rest of their workers.

So it’s certainly gonna help h hurt juniors who were doing entry-level jobs that was more gruntwork for this kind of jobs, like jobs that involve words, basically. But I don’t know that we’re gonna get to the, you know, the the doomsday revolution, nobody has a job anymore because of LLMs that’s has been sold to us.

Yeah, and I think at the end of the day, someone still needs to be responsible for the outcome. Like part of what you’re paying an attorney or your accountant for is the person who signs off on that. And whether they use a AI or an LLM or not to help them, they’re still taking that responsibility. And

There’s what’s the time that takes to be comfortable, understand the context, things like that. That’s the part that’s hard to accelerate beyond a certain amount.

Yeah, and so I mean if you take the job of software engineering, basically what what used to happen is when you were fresh out of college, you know, you would join a team and you would do a lot of small tasks to get to know the code base and and basically get people to give you feedback on those tasks and see if you were reasoning well about what you were doing. And f for these kind of entry jobs levels, it’s much harder.

It’s much harder now because you can definitely get them done by an LLM. And I think the industry needs to think about this. And they need to think about this deeply because if those junior engineers don’t have a chance to, you know, go through this learning curve. I mean, I I talk a lot with people who are in the industry about this. And I have a lot of friends who are, you know, level director and above, have eighty or a hundred, two hundred people under them.

And and the trend that we tend to see is LLMs help senior developers a lot because they’re they’re able to use judgment on what they should be doing with an LLM and what works and what doesn’t. And they had the time to establish that judgment, right? And the younger g engineers, not all of them, not all of them, not 100%. So you know, it’s it’s not, but some junior engineers struggle because

They tend to use LLMs too much and they don’t yet have, you know, enough judgment to decide if they should or not. And then, you know, bugs get caught in production much later. Then this creates a fire. Then this engineer is not trusted anymore. And and it actually is detrimental to juniors. So the trend I seem to see is it’s really good for seniors. It makes them even more productive.

It’s detrimental to juniors because they don’t know when to use the LLM and when not to. They don’t know what is, you know, tricky and where they should really tread carefully. And that’s going to be a problem in in our industry. We we haven’t addressed this at all. I mean, kids are booing in university when when there’s mention of AI. I understand. I mean, I understand that the the industry and and

It’s weird because markets are not typically, you know, thinking in those terms, right? Companies do what’s useful for them. Right now, they usually don’t optimize for what’s going to happen in 20 years. So if you tell them, hey, if you don’t hire juniors now, you’re not going to have seniors in 20 years. They’re going to tell you, well, God knows where it’ll be in 20 years, you know. So we we still have a problem with that, I think.

Yeah, I imagine as a junior engineer today it the challenge must be that you wanna get s things done at the velocity you can do with AI, but at the same time you have to develop your skill set, even if if you’re in a role. So how do you manage that conflict?

Like you were saying earlier, I think unless you’re really going and doing the thing yourself, building it and seeing how it plays out in production, you don’t learn those lessons unless

Well, and the other thing is, I mean,

software engineers, a lot of them, I mean, I know I was like that and I’m still like that. The profile of a software engineer is is typically we’re incredibly lazy. And that’s why we like software engineering, because we want the machine to do things for us. So there’s basically a tension between two things. We want to build things, but we’re also incredibly lazy. So we want to do as little work as possible to build, you know, the things that we wanna build. You know, there’s this

You know this famous saying from JFK that was like, we don’t do things because because they’re easy, we do them because they’re hard. And you know, there’s a software engineer version of that, which is we don’t do things because they’re easy, but we do things because we thought they were gonna be easy. And

Yeah. Yeah.

so there is typically this tension between I want to build things that work, but at the same time I want to spend as little energy as possible to get it to work because that’s why I like computers, they do things for me. And so

That’s where LLM is a very dangerous trap, right? Because back in my days, I wanted to build something. And if I wanted that thing built, the only way to get it built was for me to build it. And then when it didn’t work, the only thing I could do was to actually go debug it. And so given how incredibly lazy I was, I can assure you that with an LLM around.

I would have said, go figure out, you know, if you cannot do something with me while, you know, I go have beers with my friends. And and then I would have probably kept kept on pushing like that, hoping that the LLM would eventually come around, not realizing that I’m not developing my skill set. So what I’m trying to say is that I think most engineers that age, including that would have been myself, by the way,

You don’t develop your skill sets because you know you should develop your skill sets and that’s the right thing to do. You do these this grunt work because you actually want something to work and that’s what what’s motivating you, and you know that you have to go through that grunt work to make it work, right? So psychologically, there’s something that is going to be very hard for new engineers coming into this game and and hiding them.

The existence of LLMs is going to be difficult too. So I have a friend, Keith Adams. He was suggesting to have a technology that signs what a keyboard the the keys that were pressed by a keyboard

Hm.

have them signed to prove that the keyboard, you know, actually pressed the keys. The problem is, of course, you can hijack the g the signal between the thing that presses the key and

you know, the thing that does the signing. So I don’t know how you would get that done. But yeah.

Someone will just write

an LLM that presses mechanical fingers into the keyboard. Yeah. Yeah.

Exactly, you know? And so and so and and then what? You know, you add a camera to make sure that it’s

actually human fingers and then so

Yeah.
you you you know you have to it you have to be inventive. But I think it’s going to be a challenge for this generation and and I feel bad for them.
Yeah, I remember one time one day I s or I think I once spent three days figuring out why I couldn’t read a file from AWS S3. Like would I ever do that again today? No. Did I learn a lot? Yes.

Yeah. Yeah,

I mean and the classics, right? The first time one of your programs get killed by the kernel, right? And it gets killed by a signal and you don’t see anything, you just see your program that dies. And you’re like, What the fuck’s going on? And then well, you have to learn about what a kernel does and what happens when you eat too many resources and and in the process you learn, you know, how signals work and you know what you should be doing and how to catch them gracefully and how to

You know, and this is all stuff where yeah, today you would probably take an LLM, take a stack trace, or well in this case there’s no stack trace, but basically get Claude Code to figure out what’s going on and probably never learn. Or forking, you know, double forking and then figuring out why you can have, you know, zombies and whatnot and and the all this kind of stuff. There’s no way I would have learnt about any of this.

Because I didn’t care, I just wanted the program to run, and I don’t care about zombies, I just don’t want them to be there, you know, figure this out, you know.

Yeah, and you’d have to go read an like entire book of how Unix works, right? Even you couldn’t just get to the exact answer even today. Like you can, I think, in some ways, but it’s certainly a a tough challenge.

What do you think about the use of formal methods in LLMs?

Haha that’s

a really good question. I have a lot of opinions. so well, first of all, I think it’s super exciting and I think there will be a lot of value there. So don’t get me wrong, so I was the biggest fan of formal methods. I still am, but I’m still and not using them as much as as as I used to. I used to work a lot with the proof assistant Coq, which I think has been renamed to Rocq Rocq or something like that. Rocq. Is it Rocq?

I think. but basically

Mm. Yeah.

the the the stuff based on OCaml and the calculus of inductive constructions. And then I also did some model checking back in the days. So I also like this kind of formal methods. And so what I think is super exciting about formal methods is that it brings computer science closer to the field of maths, right? Which is what I was saying earlier. So in maths, what’s nice is that

you actually know the theorem you’re trying to prove and there’s a way to verify that the term the the the proof that you’re exhibiting is actually correct automatically and so you can let an LLM loose or LLM or any AI loose as long as it comes back with something you can verify then you have a problem you have a correct theorem right and so through Curry Howard right like a theorem becomes a type and a proof becomes a a term a program

Through Curry-Howard, we can have the same properties in programming, in for programming languages for for computer science, right? Where I give a spec in terms of a type, and then I don’t really care what term it comes out with, as long as the term exists, I have a type of of of this I have a term of this type. I would say things, so first of all, things are a bit different because of complexity. So usually we don’t care about

the the shape of the term, right? So if I give a spec, and let’s say for this spec I use a very rich type system. So a type system, you know, with dependent types. So I have basically all of mathematics, right? I express my type, I do care about the shape of the term, right? I don’t I don’t want a term that is exponential. I don’t want a term that, you know. So that’s one big difference with maths to begin with. The second thing

which I think is much, much more important, is that the kind of stuff that we want to do in computer science is not always easily expressed with within a spec within a formal specification. There are some places where this works beautifully. Typically it works beautifully in places where the semantics are very well established. They don’t change all that much.

And that’s it. These are the two dimensions. The semantics is very well established and it doesn’t change all that much. So the ideal candidate is an old programming language. That’s the best. You too you take a programming language that’s at least 20 years old, has not evolved all that much, or a kernel that’s old as well, hasn’t evolved all that much. You know exactly what properties you want, it’s not going change all that much. And you have very well established semantics, right? For a a compiler.

You know the semantics of the input, you know the semantics of assembly, and then you basically do your proof. Right. And so I think in these kind of cases, it’s going to work really, really well. But let me tell you my personal experience with these kind of of things, with these kinds of of tools like lean and Coq and whatever, whichever you prefer. there are many programs, so because at some point in my life in the past.

I was super excited about this when I was you know in college and right out of college. I was like, everything should be written this way. We’re gonna prove everything. And I remember my professor with a smirk tell me, what is what is everything, Julien? And so you want to prove everything. What is what is this everything that you have in mind? And and I was like, there will be no more bugs. We can just program and everything will be pure and beautiful. And I was, you know, very very excited, very young and very naive.

And I realized that, you know, I I started, you know, taking it upon myself to write programs with, you know, these kind of tools and show the properties. And and what I realized that there’s there are a ton of programs where writing down a good spec is actually hard and is actually much, much, much, much harder than writing the program itself. And the the what ends up with these kind of programs is that.

The spec becomes harder to read than the program. And what ends up happening is you don’t know what you’re proving. So you’ve rewritten this gigantic spec, and it’s great. The theorem prover says, Yep, this is correct. You have a term of this type. And then you’re scratching your head thinking, what am I doing? What is this thing? What did I prove here? You know? And so

Yes, there are some functions like you’re sorting numbers. Sure, you can write the spec for that really nicely and it’s it’s gonna be very easy to prove. Or typical data structures that have very well-defined semantics. But if you take the stuff that you’ve written in your life, you know, take a make make a pause for a second, think about you know the last big project you were working on. Imagine I asked you to specify that project using maths. Well, I can assure you that it would be

A very long endeavor. And then let’s say you are successful. You actually wrote down the spec, and you actually it it’s it’s what you wanted. Well, what’s likely to happen with every program is that it’s gonna keep on evolving, right? Like there will be different pieces, there will be different LLMs, even if everything was written by LLMs, there will be different programs, and now this API has to evolve. shit, this API has to evolve. That means that.

All the proofs that you had regarding this, some of them as mundane as the program terminates, right? Because if you’re writing in this kind of stuff, you need to prove that unless you use fuel, sure, but even for mundane things like that, you still have to prove, you know, that that things work. So now all of a sudden, a small change in API can trickle into, you know, weeks of theorem proving to get back. So

That’s why I’m both excited, but I’m also not bullish on the whole, you know, verification is gonna solve all the problems with LLMs because of those two things, right? Number one, it’s difficult for many programs to express what they do using maths. And those who say the contrary usually come from an academic background where they only do maths.

And and then once you have you know done all these proofs, okay, it’s good, but the cost of changing things is very high. You make a change, you now have to reprove potentially a lot of things. That’s what makes me skeptical for development in general.

Yeah, I I think like I know AWS has used formal proofs or part of S3’s core verification or things like that, but those are things that probably don’t change super often and the cost of getting it wrong
And also
is super high, right?

So and also, I mean,

I so just to be extra clear, I am not talking about Amazon. So I hope Amazon doesn’t sue me because I’m not talking about them. But back when I was working on verification professionally, I’ve known of companies who’ve made announcements of that sort. The core of this and that is proven da-da-da. When you know what was actually proven and how the sausage is actually made, you’re like, yeah.

That’s marketing. You you really

Yeah.
haven’t proven much here. You you have a small a subset that is so small that what you’ve proven would make anybody who is serious about this laugh. So we also must be careful with the announcement effect of an of something like that.

We’ve talked about how software is changing with AI. You’re fundamentally an optimist. Are you

Optimistic for where we’re headed in the next year, two years with everything that’s changing.

No, so I’m I’m optimistic for the long term. I think for the next year is gonna be a bumpy road, I think. Until we know where LLMs settle. I don’t know if it’s gonna be one year, two years, but I think the next two years are going to be very difficult. It’s going to be difficult to navigate because new skills, skills that were once very relevant as a software engineer won’t be relevant anymore.

So for example, I I worked a lot with security teams in the past. And a lot of their job was to review code and find exploits. And I think that now it’s pretty clear that LLMs do a really good job at this. So I don’t think that the job will disappear altogether because sometimes they have to invent new ways of hacking things, right? So for example, when they really come up with a completely new attack.

then that’s something, the kind of work that’s still going to keep around. But what’s going to be probably less of a job now is scan through code bases and identify weaknesses that remind you of an existing attack and see if you can, you know, craft together, adapt an existing attack to exploit, you know, the kind of things that you see. That job, I think, is is less is going to become a lot less relevant. and so

The pr the same is probably gonna be true for mathematicians, right? So there used to be two kind of proofs basically. There was the people with big ideas that would structure things and and you know come up with new theories that yet would let you think differently about things, like Galois, for example. And you would have proofs that were more tricks, you know, like you found the right trick and now this proof becomes. I think if you are more

Kind of person who likes to find the right trick, that’s gonna be harder for you because LLMs have basically read all the tricks that exist on the internet. And if there is an adaptation of a trick that you can use to make a proof, they they will find it. So I think that in the next two years, whether you are a mathematician or if you are a computer scientist, I don’t know about other fields, probably the same is gonna be true. Your job’s gonna change. It’s gonna change fast.

And it’s it’s it brings anxiety, right? Like you you like to hold on to the things that you know. So I think the next one or two years, bumpy road. You should hang in there and you know, realize that this is not forever, the the dust is gonna settle. But then once the dust settles, I think it’s gonna be awesome. there will be new skill sets that you’re going to develop.

a ton of the grunt work that we used to do will be will be gone. And you can focus on the interesting stuff, which is what I believe where we headed with software engineering. There are other challenges like you know how we’re going to train juniors and whatnot. but I think overall it’s going to be a bright future. It’s going to be very fun.

we’ll be able to build a lot more stuff. so I I’m excited. But yeah, the next year or two hang in there.

It like like any period of rapid change can be anxiety provoking but have have to keep looking forward to what comes beyond and the good things we can build with this technology too.
Exactly. Yeah, that’s a good way of summarizing. You you should you you said it much better than than I did. It took me five minutes to to say what you said in a sentence. There we go, there we go. Human intelligence at work,
I had your prompt first. I was I was just summarizing like a like an LLM.
right there.
Right. Well, Julien, thanks again for joining us. It was great to have you on today.
Thank you for having me. This was a ton of fun.
And we’ll have all of Julien’s links and info so you can find him in the show notes. And thanks again for joining us for the show. We’ll see you soon.
Thanks everybody.