Notwithstanding the duplication of these posts across social media, OpenAI, and Anthropic ("it's all the model, they just tell it to keep going" if you beat anything with RL enough ... it's going to do the thing)
Here's my issue with this post:
> True to the spirit of the challenge, they didn’t use millions of dollars in computer power. They used Fable 5.1, working within Claude Science, a platform scientists can pay to use.
Okay, billions of dollars have been poured into these agentic LMs, right? Each training run to get the next increment is costing millions of dollars?
This feels like an obvious jab at Navier-Stokes, but where we get to shift the numbers around to hide where the compute actually is being spent ... compute is being spent. It's either being spent in amortization to make the search smarter ahead of time, during training, or its being spent after.
Also love: scientists get to pay Anthropic to work within their special science harness to do science. That's exactly what I dreamed of doing when I pursued physics in undergrad, one or two companies holding the keys to "progress" for a monthly subscription price.
> Also love: scientists get to pay Anthropic to work within their special science harness to do science. That's exactly what I dreamed of doing when I pursued physics in undergrad, one or two companies holding the keys to "progress" for a monthly subscription price.
I get this anxiety, and am largely an AI skeptic, but at one point there were only a handful of computers in the world too (same for batteries, or engines, or crucibles, or stills -- it goes way back), and the organizations that had them had a stranglehold on progress in the field, as did the small number of companies who knew how to make them. It got better as they got cheaper and more plentiful.
I guess my point is that there are more important anxieties to feed when it comes to LLMs and the current state of the world.
> This feels like an obvious jab at Navier-Stokes, but where we get to shift the numbers around to hide where the compute actually is being spent ... compute is being spent. It's either being spent in amortization to make the search smarter ahead of time, during training, or its being spent after.
I think that argument is recursive? These posts aren't very complicated for either of us, but they're written on devices that are fabricated with billions of dollars of semiconductor equipment. At what point do we just acknowledge that we stand on the shoulders of giants?
To me, the distinguishing factor is that the expense not special-purpose but upfront. The model here is trained without foreknowledge of what problems it will solve. Solutions like nine loops are genuine expressions of a pre-existing model capability, even if that capability has not pre-existed for very long.
Oh I agree with you! I just don't see "we're standing on the shoulders of giants" in most of these marketing blog posts?
If I'm wrong here, I'd love reference links. I think of these companies as trying to inspire the idea that Claude (or GPT) are these special alien entities, in a sense?
Divide the compute of your argument (pre-training, training, post-training) through everything this model now can do and it will not look that bad at all.
> Also love: scientists get to pay Anthropic to work within their special science harness to do science. That's exactly what I dreamed of doing when I pursued physics in undergrad, one or two companies holding the keys to "progress" for a monthly subscription price.
The moat is very limited. Harnesses aren't crazy hard to engineer. Open models are quite capable.
The training costs get rolled into the usage prices. It's not hiding anything to talk about the cost of usage without the cost of training, any more than I'd be hiding something by talking about the price of a $1,000 CPU without mentioning the tens of billions of dollars in R&D and infrastructure needed to create it.
What a weird thing to be butthurt about. You don't have to pay them. Do it the old fashioned way, with elbow grease and pots of coffee. Or invest in local AI.
Or embrace the future and realize that you couldn't imagine everything that would unfold, when you pursued your undergrad.
There was a time when a generation of hackers got (rightfully) worked up about the Microsoft tax for every PC sold. It's not hard to see that somebody gets mad if they believe that an Anthropic/OpenAI tax is about to become the standard when doing any serious Physics/Math/... research or writing code.
The term "hackers" didn't just apply to those of us who wiped the thing off first chance they got. Folks working in IT of large corps which had fleets of a 5-digit numbers of PCs to administer and for each of them, Microsoft took their cut.
Just because a description doesn't apply to you personally doesn't mean it's misrepresenting things.
One of the most interesting aspects of MiMo 2.6 is that they shared their RL costs, sub $5M (yes, million)
This stuff is going to get a lot cheaper, just like Stable Diffusion
I for one find the incessant side questing the moment something goes awry to be very annoying. Please stop and ask the human for clarification or guidence
I'm always surprised by statements about "things we don't need to learn anymore" with AI.
It's sort of a litmus test for how little someone understands how learning in humans works or AI itself even. "Agentic" AI acts as a mirror: the more insight have yourself, the more powerfully you can pull the distribution ... the more you get out of it. (there's a bloodborne-inspired parable in here somewhere ...)
I think it's why the software from AI companies has "garbage" qualities. They are assuming that AI is going to fill in skills ... when it is a reflective amplifier.
But back to the discussion of "things we don't need to learn anymore": do we go to the gym, and say ... oh I don't need to do pull ups anymore, because there's an assisted pull up machine and I can just set it to my weight ...
> "Hey Claude, can you be smarter than me and tell me what I should tell you to get the thing I don't know I want yet?"
I'm so glad you asked! Many smart people are now eating Snickers Bars(tm)! For you, I think, to get ahead of this trend, it would be the perfect smart person choice right now. It's nutty and has this amazing new invention called Nougat and chocolate!
Here's how it works. First you have to use your fingers to tear open the wrapper. Don't worry, the wrapper isn't going to hurt you. It might be a little effort, but you'll get it. Then you take a bite. Try to use your back teeth to chew it a little. Yeah, I know it's work, but it's good for you. And then just swallow it down!
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.
reply