Here's the one simple trick that fixes everything:
- Use the code that your agents write in anger.
There you go. Do I know when my agents fuck up? Yes, I absolutely do -- because I'm a user of the code I have my agents write, and I ask things like "why is it taking 50 ms to start this program ..." and then I go in and find stupidity, and excise it. I do this over and over again.
Is it faster than writing it out by hand? Maybe! It's definitely a different perspective.
Start behaving like a baby "why, why, why" and then do a bit of reading, and you'll be fine.
A lot of these blog posts seem like they're aimed at software written by B2B companies who don't even use their own software ...
I think someone can follow "good practices" with a team and get to a bad place, especially with such a novel product (as AI coding agents).
But taking Claude Code as the product of this style of thinking -- who is Claude Code for? Is it for everyone in the world? Well, if you look at the feature velocity, it seems like the answer is intended to be yes ... Claude Code is trying to solve every problem in software development in the world, all at the same time.
So I question the "user model" here.
Here's another thing that is true about Claude Code: it's among the most inconsistent and buggy pieces of software I've ever encountered.
- You can move the cursor with the mouse in the composer, but not in AskUserQuestion?
- When agents spawn subagents, the model name is inherited from the main agent, and seemingly none of the (4! yes, 4!) subagent tools seem to get this right (except for Explore, which seems to be fixed to a weaker model)
- Sometimes, when my usage limit halts, my agents will pick up when it refreshes (within ~2 hours or something) ... other times, nope -- even within the usage limit?
This is a sampling of my own experiences using this thing frequently. Are these sorts of details not important? Maybe not: I'm not at the level of this team, and may never be.
But I think it's a reflection of agentic engineering ... a somewhat embarrassing one, from my perspective. It paints a picture of a team who can't quite get the details right, even with the assistance of purported extremely powerful AI tools, even internal ones which we don't have access to?
I think when people look back on 2025 -- Boris is going to have his name right there in the books ... Claude Code, coding agents -- Anthropic (& Boris + team) made the first move.
But now it's 2026, and people know how harnesses work, and heavy lies the crown.
@LiamPowell the author is clearly aware of formal verification, they've written several implementations of dependently typed languages, and ... despite the presentation of their work, which has some obvious flaws (as can be judged by reception) ... their many comments indicate that they know what they are talking about.
Your post is setting up a strawman between automatic formal verification and formal verification using interactive theorem provers ... obviously there is a spectrum, and Ada/SPARK are navigating the space to try and automate much of the work required to automatically dispatch with obligations to prove (computable) properties about programs.
Bend2 is a QTT -- it's dependently typed, and comes from the lineage of systems which are focused on being expressive enough to formalize mathematics.
Of course you need to build a somewhat significant "standard library" of theorems, tactics (as metaprograms), etc ... to approach what is built into the compiler in Ada. These are different approaches with different trade offs.
Your post isn't clear, you don't go into any of these details ... why did you post this? Do you think this is clear writing?
> the author is clearly aware of formal verification, they've written several implementations of dependently typed languages
I'm not familiar with the author, I just saw the language posted the other day. I'll add a note to the top.
> These are different approaches with different trade offs.
Why would we want the tradeoff where the LLM has to write significantly more code and where the specification needs to be more complicated? If the author is aware of the state of the art then I think they made a poor choice, but that's not the point.
> Your post isn't clear, you don't go into any of these details
Bend just serves as a useful example, my general point is about how people will vibe-code a solution without an understanding of the field, leading to worse results than if they spent a little while understanding the field and then vibe-coded their thing.
Perhaps because their concerns are different? Similar reasoning: "why invest in dependently typed languages over SMT solvers? SMT solvers are automatic, and it is way easier to add annotations to my programs"
The answer is that these technologies are not universal in trade off space.
Of course, if you can have an LLM prove something by dispatch to an SMT solver ... you want to do that (and, indeed, LLMs do sometimes do this even when working on Lean proofs)
But the space of statements that you can prove using verification with SMT is smaller than dependently typed systems.
Also, Ada/SPARK are very good and robust -- they've been around for ~50 years ... but there's been a significant amount of work in formal verification since then, right? I would be more clear that Ada/SPARK are state-of-the-art for "mission critical software" (and have been for many years), but there's been a lot of research work in formal verification of low level programming since then (Low*, for instance)
I'm assuming you have not spent a lot of time trying to prove stuff about non trivial programs if the trade offs between SMT based approaches and interactive theorem provers are not clear to you.
SMT solvers are highly automated, but very opaque and hard to debug. Interactive theorem provers can scale to larger problems and harder properties at the cost of increased manual proof burden. The ever increasing ability of llms to write proofs in a theorem prover has in recent years tipped the balance significantly towards preferring itp based approaches over pure SMT ones. The current state of the art for program verification is probably a mix of llm and traditional (tactics, SMT, etc.) proof automation inside an itp.
ATPs go quite a bit beyond what a SMT solver can do, however you're not stuck with just using ATPs when they are supported. You can still allow for proofs to be manually written with an ATP doesn't work, and in fact SPARK allows for this with Rocq.
Most of what I have to prove is floating-point code where a manual proof is too much of a headache to ever attempt though.
If you're going to insinuate that the author of Bend2 doesn't understand PLs and formal verification, you should do so with some proof and not a hot take dunk.
I think it's fine to critique the language and the approach without criticizing the author and I hate that this site has become Tech Drama News, like the worst parts of Twitter.
Yes, I didn't realise how much it comes off as a critique of the author personally when I wrote it. I have added a note to that effect to the top of the article.
conversations on this site about formal methods are currently absolute cess pits of dunning kruger and confidently stated yet highly misinformed takes from those with close to little experience in the field.
I think sadly all big conversations on this site are like this these days. It didn't used to be like that sadly. Z3 and some early Lean threads used to be great.
You clearly don't know shit about the whole topic, yet attack an open-source project's author who wasn't even the one posting his own project..
> Why would we want the tradeoff where the LLM has to write significantly more code and where the specification needs to be more complicated? If the author is aware of the state of the art then I think they made a poor choice, but that's not the point.
Because code is trivially cheap now. LLMs churn out a shitton of code at pennies, and as technology improves their per-line cost will continue to decrease. A proof has to be written once and it's never read again. It's only important property is that it is machine-verifiable - from then on only the signature matters. Meanwhile speed of compilation matters, so an obvious tradeoff was made by the author.
> my general point is about how people will vibe-code a solution without an understanding of the field, leading to worse results than if they spent a little while understanding the field and then vibe-coded their thing.
This is clearly not the case here, and even if it were, it's still a better thing than vibe-blogging clickbait shit with extra amount of Dunning–Kruger. Calling out an author who clearly works in the field for a decade or more for not knowing the topic...
My read on this, after ingesting a good amount of content on the history, is:
- this Bend is not really related to the old Bend (only in name)
- this Bend doesn't really have anything to do with interaction combinators
- this Bend is a QTT, with a change to affinity which enforces a good performance property for GPUs
- the "higher order at comptime" is neat, reminds me of Andras Kovacs' work on 2ltt and staging in dependently typed languages.
- this Bend is likely to be good at "balanced recursive computations on ADT", and can parallelize them ... but won't be as good as CUDA or e.g. Futhark on dense rectangular array computations
- performance needs improvement in the scheduler, to possibly help with balanced work (looking at the n queens and symbolic regression numbers)?
How are you going to handle search or synthesis over irregular structures (SupaGen)?
Here's what Victor wrote about inets in Bend2 (on X):
> interaction combinators still parallelize better than anything else, but the graph overhead prevents us from compiling to maximally efficient assembly. bend2 is basically inets without the overhead. in a way, inets live in it architecturally, but they don't exist at runtime
From what I understand, the main difference between lambda calculus and inets is that in LC you can refer to a binding multiple times for free, i.e. call same closure multiple times, etc. In inets, you can't - they are more like physical wires where each reference costs. You can definitely see inets in Bend design here (from the guide):
> A closure is affine: it can be called at most once, even when everything it captures is Data. Only top-level definitions can be called freely.
So programming in it might be very different from the normal functional programming. Seems like a big limitations. But I guess that's what lets it run without GC, on GPUs, etc.
aww man. I remember following victor in college. I mean pivots gotta pivot, and this is probably a better one for business, but always thought the interaction combinator framework was cool
AI is extremely useful, but it’s also extremely easy to fool yourself into thinking you understand what is going on without really understanding. This is often true with the code, but also for math and science concepts, etc.
Not many professions are formally trained to be cognizant of this lack of understanding, and how to confront it.
Usage of AI in collaborative settings is an amplifier of these issues, especially if someone doesn’t realize they don’t understand: they couldn’t teach or explain the concepts they use, or be forced to work with them malleably in a way that an expert or researcher would.
If you are cognizant of your lack of understanding, you can remedy it by slowing down and teaching yourself. This is required to make better use of AI in the domain of interest!
But you can’t have all things at once: you can’t move at speed with AI, collaborate effectively, and understand what is going on as an expert would. It is not physically possible for a human brain.
> But you can’t have all things at once: you can’t move at speed with AI, collaborate effectively, and understand what is going on as an expert would. It is not physically possible for a human brain.
I think the article's point is more nuanced. Short term, the human brain as the "conductor" can keep up and an expert can see whether the machine did a good job and course correct if necessary. Over time though that degrades more and more.
> But you can’t have all things at once: you can’t move at speed with AI, collaborate effectively, and understand what is going on as an expert would. It is not physically possible for a human brain.
Very well put. You can pick one or two, but not all three.
No, it is a shocking level of incompetence given the conveyed seriousness of the work by these labs.
So yes, models are getting better. Ask yourself: if you know that to be true, would you act the same way that the teams did in the public post mortems?
- Use the code that your agents write in anger.
There you go. Do I know when my agents fuck up? Yes, I absolutely do -- because I'm a user of the code I have my agents write, and I ask things like "why is it taking 50 ms to start this program ..." and then I go in and find stupidity, and excise it. I do this over and over again.
Is it faster than writing it out by hand? Maybe! It's definitely a different perspective.
Start behaving like a baby "why, why, why" and then do a bit of reading, and you'll be fine.
A lot of these blog posts seem like they're aimed at software written by B2B companies who don't even use their own software ...
reply