> With dynamic languages where the model has a ton of training data, like Python, the agents are really good at writing code that just works.
I'm confused how the former supports the latter here.
Surely, you mean that LLMs are not the right kind of "AI". Languages like Haskell expose how fundamentally porous LLMs are with information.
Admittedly I'm not much better, Agda has some crazy scoping rules at times and its operators are a mess, so much worse than Haskell, but at least I don't have to re-learn from scratch after every compaction.
So, I could write what I want in haskell, and it's faster for me than to have an LLM do it. The haskell would be high-level enough and precise enough to describe what I want the program to do with less iterations than I'd have with an LLM writing code, finding its own bugs, fixing them, then having me ask it what it did, tell it what to do differently, etc.
Direct control is very powerful. LLMs take that away from us, in exchange for a great speedup. But perhaps we can use LLMs to give it back to us by making our actual programming languages more powerful.
Here's one rough example that is related to this direction:
A common convention in Lean is to write essentially two versions of a function, with a theorem proving their equality or correspondence.
So you can write a more demonstrative version that is more easily understood, which you can treat sort of as a spec that all other implementations must satisfy. And then you can set the agent loose to do whatever nastiness it wants to do to improve performance.
Here's a fun write up from someone doing just this with zip file compression: https://kim-em.github.io/blog/2026-7-24-why-lean-is-faster-t...
Token efficiency is specifically the place where strict languages get a little trickier. With dynamic languages where the model has a ton of training data, like Python, the agents are really good at writing code that just works. You still have challenges there, but they're just different than the challenges you hit with a language like Haskell/Lean/Agda etc. With Lean, for example, the amount that they agent might think it needs to prove for a relatively trivial operation can lead to an absurd amount of code. It sort of plays perfectly towards current agent weaknesses, where agents can run off and reinvent a lot of machinery and build unnecessarily complex abstractions.
And those iterations have a cost. Even if the final artifact is more terse, the path to getting there can involve a huge amount of backtracking and rewriting and off-by-one syntactic corrections.
Ultimately, a lot of this comes down to developer experience. Getting useful error messages for the agent, having fast compile times so that the agent can iterate quickly, providing useful utilities for debugging, etc. There was a popular blog post specifically about Haskell that generally makes this point--the Haskell language is, in a vacuum, ideal in a lot of ways for AI, but the Haskell developer experience and ecosystem made it hard for this team to build with it via agents: https://avi.press/posts/2026-07-10-after-7-years-in-producti...