5 ms·

I encourage everyone to RTFA and not just respond to the headline. This really is a glimpse into where the future is going. I've been saying "the last job to b

by madrox 8mo ago

I encourage everyone to RTFA and not just respond to the headline. This really is a glimpse into where the future is going. I've been saying "the last job to be automated will be QA" and it feels more true every day. It's one thing to be a product engineer in this era. It's another to be working at the level the author is, where code needs to be verifiable. However, once people stop vibing apps and start vibing kernels, it really does fundamentally change the game. I also have another saying: "any sufficiently advanced agent is indistinguishable from a DSL." I hadn't considered Lean in this equation, but I put these two ideas together and I feel like we're approaching some world where Lean eats the entire agentic framework stack and the entire operating system disappears. If you're thinking about building something today that will still be relevant in 10 years, this is insightful.

charlieflowers 8mo ago
> "any sufficiently advanced agent is indistinguishable from a DSL." I don't quite follow but I'd love to hear more about that.
- esafak 8mo ago
  https://en.wikipedia.org/wiki/Clarke's_three_laws https://en.wikipedia.org/wiki/Clarke's_three_laws
  - charlieflowers 8mo ago
    No i get the clarke reference. But how is an agent a dsl?
    - whattheheckheck 8mo ago
      Maybe not an agent exactly but I can see an agentic application is kind of like a dsl because the user space has a set of queries and commands they want to direct the computer to take action but they will describe those queries and commands in English and not with normal programming function calls
- jpollock 8mo ago
  If the llm is able to code it, there is enough training data that youight be better off in a different language that removes the boilerplate.
- madrox 8mo ago
  If you give an agent a task, the typical agentic pattern is that it calls tools in some non-deterministic loop, feeding the tool output back into the LLM, until it deems the task complete. The LLM internalizes an algorithm. Another way of doing it is the agent just writes an algorithm to perform the task and runs it. In this world, tools are just APIs and the agent has to think through its entire process end to end before it even begins and account for all cases. Only latter is turing complete, but the former approaches the latter as it improves.
- thinkling 8mo ago
  My read was roughly that agents require constraining scaffolding (CLAUDE.md) and careful phrasing (prompt engineering) which together is vaguely like working in a DSL?
bwestergard 8mo ago
I am as enthusiastic about formal methods as the next guy, but I very much doubt any LLM-based technique will make it economical to write a substantial fraction of application software in Lean. The LLM can play a powerful heuristic role in searching for proof-bearing code in areas where there is good training data. Unfortunately those areas are few and far between. Moreover, humans will still need to read even rigorously proved code if only to suss out performance issues. And training people to read Lean will continue to be costly. Though, as the OP says, this is a very exciting time for developing provably correct systems programming.
- zozbot234 8mo ago
  LLMs are writing non-trivial math proofs in Lean, and software proofs tend to be individually easier than proofs in math, just more tedious because there's so much more of them in any non-trivial development. Some performance issues (asymptotics) can be addressed via proof, others are routinely verified by benchmarking.
- madrox 8mo ago
  This assumes everything about current capabilities stay static, and it wasn't long ago before LLMs couldn't do math. Many were predicting the genAI hype had peaked this time last year. If you want it to be a question of economics, I think the answer is in whether this approach is more economical than the alternative, which is having people run this substrate. There's a lot of enthusiasm here and you can't deny there has been progress. I wouldn't be so quick to doubt. It costs nothing to be optimistic.
  - candiddevmike 8mo ago
    > and it wasn't long ago before LLMs couldn't do math They still can't do math.
    - Hammershaft 8mo ago
      Pro models won gold at the international math olympiads?
fmbb 8mo ago
There are still no successful useful vibe codes apps. Kernels are pretty far away I think.
- GoatInGrey 8mo ago
  To be fair, Claude Code is vibe-coded. It's a terrible piece of software from an engineering (and often usability) standpoint, and the problems run deeper than just the choice of JavaScript. But it is good enough for people to get what they want out of it.
  - bunderbunder 8mo ago
    But also, based on what I have heard of their headcount, they are not necessarily saving any money by vibecoding it - it seems like their productivity per programmer is still well within the historical range. That isn’t necessarily a hit against them - they make an LLM coding tool and they should absolutely be dogfooding it as hard as they can. They need to be the ones to figure out how to achieve this sought-after productivity boost. But so far it seems to me like AI coding is more similar to past trends in industry practice (OOP, Scrum, TDD, whatever) than it is different in the only way that’s ever been particularly noteworthy to me: it massively changes where people spend their time, without necessarily living up to the hype about how much gets done in that time.
  - jmathai 8mo ago
    > But it is good enough for people to get what they want out of it. This is the ONLY point of software unless you’re doing it for fun.
- bonoboTP 8mo ago
  This is a very strange statement. People don't always announce when they use AI for writing their software since it's a controversial topic. And it's a sliding scale. I'm pretty sure a large fraction of new software has some AI involved in its development.
  - qsera 8mo ago
gwern 8mo ago
> I encourage everyone to RTFA and not just respond to the headline. This is an example of an article which 'buries the lede'†. It should have started with the announcement of the new zlib autoformalization (!) https://leodemoura.github.io/blog/2026/02/28/when-ai-writes-the-worlds-software.html#a-sign-of-things-to-come https://leodemoura.github.io/blog/2026/02/28/when-ai-writes-... to get you excited. Then it should have talked about the rest - instead of starting with rather graceless and ugly LLM-written generic prose about AI topics that to many readers is already tiresomely familiar and doubtless was tldr for even the readers who aren't repelled automatically by that. † or in my terms, fails to 'make you care': https://gwern.net/blog/2026/make-me-care https://gwern.net/blog/2026/make-me-care
kubanczyk 8mo ago
> RTFA Sigh. Is there any LLM solution for HN reader to filter out all top-level commenters that hadn't RTFA? I don't need the (micro-)shitstorms that these people spawn, even if the general HN algo scores these as "interesting".

by madrox 8mo ago

charlieflowers 8mo ago

> "any sufficiently advanced agent is indistinguishable from a DSL." I don't quite follow but I'd love to hear more about that.

esafak 8mo ago
https://en.wikipedia.org/wiki/Clarke's_three_laws https://en.wikipedia.org/wiki/Clarke's_three_laws
- charlieflowers 8mo ago
  No i get the clarke reference. But how is an agent a dsl?
  - whattheheckheck 8mo ago
    Maybe not an agent exactly but I can see an agentic application is kind of like a dsl because the user space has a set of queries and commands they want to direct the computer to take action but they will describe those queries and commands in English and not with normal programming function calls
jpollock 8mo ago
If the llm is able to code it, there is enough training data that youight be better off in a different language that removes the boilerplate.
madrox 8mo ago
If you give an agent a task, the typical agentic pattern is that it calls tools in some non-deterministic loop, feeding the tool output back into the LLM, until it deems the task complete. The LLM internalizes an algorithm. Another way of doing it is the agent just writes an algorithm to perform the task and runs it. In this world, tools are just APIs and the agent has to think through its entire process end to end before it even begins and account for all cases. Only latter is turing complete, but the former approaches the latter as it improves.
thinkling 8mo ago
My read was roughly that agents require constraining scaffolding (CLAUDE.md) and careful phrasing (prompt engineering) which together is vaguely like working in a DSL?

bwestergard 8mo ago

I am as enthusiastic about formal methods as the next guy, but I very much doubt any LLM-based technique will make it economical to write a substantial fraction of application software in Lean. The LLM can play a powerful heuristic role in searching for proof-bearing code in areas where there is good training data. Unfortunately those areas are few and far between. Moreover, humans will still need to read even rigorously proved code if only to suss out performance issues. And training people to read Lean will continue to be costly. Though, as the OP says, this is a very exciting time for developing provably correct systems programming.

zozbot234 8mo ago
LLMs are writing non-trivial math proofs in Lean, and software proofs tend to be individually easier than proofs in math, just more tedious because there's so much more of them in any non-trivial development. Some performance issues (asymptotics) can be addressed via proof, others are routinely verified by benchmarking.
madrox 8mo ago
This assumes everything about current capabilities stay static, and it wasn't long ago before LLMs couldn't do math. Many were predicting the genAI hype had peaked this time last year. If you want it to be a question of economics, I think the answer is in whether this approach is more economical than the alternative, which is having people run this substrate. There's a lot of enthusiasm here and you can't deny there has been progress. I wouldn't be so quick to doubt. It costs nothing to be optimistic.
- candiddevmike 8mo ago
  > and it wasn't long ago before LLMs couldn't do math They still can't do math.
  - Hammershaft 8mo ago
    Pro models won gold at the international math olympiads?

fmbb 8mo ago

There are still no successful useful vibe codes apps. Kernels are pretty far away I think.

GoatInGrey 8mo ago
To be fair, Claude Code is vibe-coded. It's a terrible piece of software from an engineering (and often usability) standpoint, and the problems run deeper than just the choice of JavaScript. But it is good enough for people to get what they want out of it.
- bunderbunder 8mo ago
  But also, based on what I have heard of their headcount, they are not necessarily saving any money by vibecoding it - it seems like their productivity per programmer is still well within the historical range. That isn’t necessarily a hit against them - they make an LLM coding tool and they should absolutely be dogfooding it as hard as they can. They need to be the ones to figure out how to achieve this sought-after productivity boost. But so far it seems to me like AI coding is more similar to past trends in industry practice (OOP, Scrum, TDD, whatever) than it is different in the only way that’s ever been particularly noteworthy to me: it massively changes where people spend their time, without necessarily living up to the hype about how much gets done in that time.
- jmathai 8mo ago
  > But it is good enough for people to get what they want out of it. This is the ONLY point of software unless you’re doing it for fun.
bonoboTP 8mo ago
This is a very strange statement. People don't always announce when they use AI for writing their software since it's a controversial topic. And it's a sliding scale. I'm pretty sure a large fraction of new software has some AI involved in its development.
- qsera 8mo ago

gwern 8mo ago

> I encourage everyone to RTFA and not just respond to the headline. This is an example of an article which 'buries the lede'†. It should have started with the announcement of the new zlib autoformalization (!) https://leodemoura.github.io/blog/2026/02/28/when-ai-writes-the-worlds-software.html#a-sign-of-things-to-come https://leodemoura.github.io/blog/2026/02/28/when-ai-writes-... to get you excited. Then it should have talked about the rest - instead of starting with rather graceless and ugly LLM-written generic prose about AI topics that to many readers is already tiresomely familiar and doubtless was tldr for even the readers who aren't repelled automatically by that. † or in my terms, fails to 'make you care': https://gwern.net/blog/2026/make-me-care https://gwern.net/blog/2026/make-me-care

kubanczyk 8mo ago

> RTFA Sigh. Is there any LLM solution for HN reader to filter out all top-level commenters that hadn't RTFA? I don't need the (micro-)shitstorms that these people spawn, even if the general HN algo scores these as "interesting".