> The problem is that vibe coding makes it possible to build a substantial solution before learning enough about the problem to recognise that a much better solution exists.

This example and Bend aside, I find this to be the biggest struggle with the perceived intelligence we have today. It's great at producing something that works, but it is not great at calling you out when you don't know what you don't know.

It's not able to educate and course correct you unless you have great self awareness and discipline.

That said, I think this goes for everything, it's easy to fall into this trap because it is very human. We simply don't know what we don't know, so it's not uncommon to revisit an old solution only to be enlightened that there is now new information that allows you to replace it with something much better.

I don't think anything here is new or changed, if anything changed is really just the rate that we experience this. LLMs make it easier and faster for the feedback cycle to happen.

Now back to Bend, I think putting your work out there and being unapologetic about it, open source even, and willing to take feedback, will go a long way.

I am more worried about the many closed source implementations of LLM built products that are being sold and people are depending upon that don't get this great criticism from many different thinking heads.

The original discussion about the project (https://news.ycombinator.com/item?id=49746163) is very weird. Lots of call-outs about how the author is some sort of celebrity and random accounts vouching for him, with little discussion on the substance.

Not even the demo on that release works well.

> The field in question is formal verification. It’s notable that those two words appear nowhere on Bend’s webpage or in its codebase. The developer has built an entire language around a field seemingly without realising that said field exists.

I checked the developer's X account, they have written numerous posts about formal verification, so this specific claim ("without realising that said field exists") seems to be false.

> Where this differs from Bend is that what we have supplied here is everything required to prove the correctness of the program, without having a LLM waste time and tokens on building up a 442 line proof from first principles. We can run GNATprove and get: `Success: all checks proved (12 checks).`

GNATprove uses SMT solvers, meaning it's basically a brute force proof system.

Yes, brute-force proofs are easier than symbolic proofs (lean, bend, etc.) because you don't have to supply a proof. It's all automatic.

But brute-force proofs don't scale to nearly anything of interest, which is why formal verification has been a niche field for 30 years, until now where LLM can write _actual_ proofs.

Pretty impressive to accuse the author of not knowing formal verification when even minutes of research would immediately prove the opposite (https://x.com/victortaelin/status/2100942399132312059?s=46, https://x.com/victortaelin/status/2100374221671051472?s=46).

I haven't looked into Bend 2 in detail, but it seems a bit harsh to call it "horribly broken or decades behind the current state of the art". Clearly there is a problem with formal verification languages and there is a demand for something else in that area, and the problem is the usability and syntax. I don't want to have to learn something that looks like Haskell, or to have to wrap my head around Curry-Howard correspondence. I don't want to write my conditions in something that looks and feels like C++ template metaprogramming. I recall a Hello World in something like Coq a few years ago which basically started with "first, we construct the Peano integers", and then they used this to prove that some calculation was bounded - because it seems they couldn't represent integers natively?

I just want to be able to write C#, JavaScript or whatever, and then tack on preconditions, checks and so on with the same syntax. Dependent typing and design by contract for the masses.

> The author of Bend has completely missed that this is the current standard in the field of formal verification, if they even know that this field exists at all. They have instead come up with this whole system requiring verbose specifications and even more verbose proofs. A little research before vibe-coding an entire language and compiler could have substantially improved the result because the author would have known what to ask for.

> This example matters beyond Bend, vibe-coding makes it makes it far too easy to implement a design that’s horribly broken or decades behind the current state of the art because you can immediately get a result without ever having to do any research. If you ask a LLM for a language where it’s possible to prove that a function is formally correct by building up a proof from basic principles then it will happily do so, it will never stop to suggest to you that computers can already build complex proofs without the need for a LLM and eliminate 99% of the work. It will never tell you that what you’re building already mostly exists as work that you can build on.

---

That's why all your LLM requests to build something substantial should start with "run prior work research first". Of course, at some point everything converges (if we share our outputs open-source) and then we may have solid standard patterns and libraries and do not need to waste trillions of tokens globally to rebuild the same minor, fundamental things, each one in their silent little silo.

IF we share, it will be of course to the monetary detriment of LLM providers who will have less income overall, and of course now they can't repackage anymore all our collective input, thoughts, human 'thinking traces' that they collect in their meta-data, as their new 'innovations' any more to inflate IPOs / stock prices.

> A little research before vibe-coding an entire language and compiler could have substantially improved the result because the author would have known what to ask for.

A little research before writing and publishing a personal attack like this could have substantially improved the result because the author would have known what they're writing about

Victor is not a formal verification noob as this article suggests

Some noteworthy lines from the README.md[0]:

> - The compiler (not kernel) is 99% AI-written and has not been fully audited yet.

> - Strings are linked lists of characters, so text processing is slow.

[0]. https://github.com/bendlang/bend/tree/main

If you have to write LAWS.bend which is pure code describing the laws then it isn't basically like those old days of writing unit tests and that too tests first hence the TDD?

So what is the unique idea here except a vibe coded compiler that generates C and everything else is handled by clang+llvm?

From README.md:

>The compiler (not kernel) is 99% AI-written and has not been fully audited yet.

Also, why the compiler is not written against and with LAWS.md so that no audit is required at all?

> It will never tell you that what you’re building already mostly exists as work that you can build on.

It will if you remember to ask it. I've got into the habit of starting any new project with a session where I ask a search-enabled LLM to help me figure out what the prior art for a problem is. It's saved me quite a bit of time.

I've been thinking about this a lot lately, because I've noticed a trend in my own life that has happened countless times: I have a tendency to look at problems that others in different fields have found difficult to solve, and think I have a great idea that could change that field. And then I push to develop my solution to that problem, run into real world problems with my solution, refine and adapt, try a different solution, run in a loop until I settle on the fact that the people who are in those fields also have great ideas, they just are more aware of the constraints and that's the reason why the hard problems don't have easy solutions.

There is an absolutely enormous amount of hubris to being an engineer. I don't necessarily think its a bad thing...a certain amount of hubris is necessary for progress to be made. Our minds are creative and we can come up with amazing things, but something in there always makes us think we can do it better than the people who are stuck doing it daily. We fool ourselves into thinking they're too stuck in their mindset to have a more creative solution.

And the funny thing about LLMs is that while they can enable our competence, they enable our hubris even more.

I am a total outsider when it comes to this topic, but it reads like the author is doing the thing they are accusing the Bend 2 guy of. Good juicy reading while I sip my coffee!

I haven't seen a language launch this controversial on HN since V-lang in 2019.

Glad we finally have some new drama to follow, definitely more entertaining than AI news.

"The developer has built an entire language around a field seemingly without realising that said field exists."

That is incredibly funny.

Here's a talk about formal verification I made 7 years ago @ DevCon:

https://www.youtube.com/watch?v=0fg1QbeeqNU

Here's Cedille Core, my implementation of Aaron Stump's self types, a Computer Science professor who taught me a lot, ~8 years ago:

https://github.com/VictorTaelin/Cedille-Core

I also implemented Kind-Lang 5 years ago, way before LLMs:

https://github.com/higherorderco/kind

I dropped out of Federal University of Rio de Janeiro to study this subject independently, because I was passionate about it, and I spent nearly 10 years doing so, daily, on weekends. That's what I do.

Bend proofs being verbose has nothing to do with me not knowing that inference, unification, or program search exists. Kind had these, 5 years ago. In fact, I've also been researching the later, and I built SupGen, which overperforms every published symbolic program synthesizer in the literature by 10x or so. This is unpublished yet, but you can find my posts about it 2 years ago on X (I'm @VictorTaelin).

So, why is Bend verbose???

Because it makes it fast. It is intentional. It is my vision that a good proof language should be fully explicit, because this reduces proof-checking time significantly. That is what makes Bend realistically 10x-100x faster than every alternative.

But wouldn't that mean it is much harder to write it?

No. As you said it yourself, we have tools that can fill these proofs today! Not just AI models. You can apply these tools to produce Bend proofs, while the language itself remains a thin, dumb proof kernel that does one thing, and does it well.

If nobody is reading these proofs (because they're written by AI and automated tools), then, it is, in my opinion, irrelevant, as proofs will eventually become a layer nobody looks at, just like generated assembly.

Of course, I could be wrong here!

But it is misleading, if not just a bit malicious, to claim I "vibe-coded" a language without knowing about a field I've spent a decade researching about.

Every single part of Bend is an intentional choice I made after considering every alternative. I use LLMs to fill code after I make all hard architectural decisions because they type faster than me, and I'd rather spend my time doing useful experiments than typing trivial functions, even though I could.

Incidentally, deciding what I should NOT include took me way more time and effort than any line that was shipped, and there are perhaps millions of lines of code, manually written by me, that I threw away, backing up these 4k that went into the final design. An artist once told me you must first paint a Rembrandt before you can draw a cartoon that's simple in the right way, yet that might mislead someone who has never drawn into thinking you don't know what you're doing. I guess.

> The problem is that vibe coding makes it possible to build a substantial solution before learning enough about the problem to recognise that a much better solution exists

As a software developer we should fear chasing "better" solutions, that path always lead to procrastination, "kitchen sink" and probably not what users wants. "Good enough" should suffice in most cases. Sure if you are building a super mega critical software to land a plane or something like that, is different. But every day software, shouldn't be treated like "carved in stone" and stuff that should last a 1000 years. Code can be cheap now (calling it "vibe coding" doesn't help).

You can create or modify something quite fast now. Better to focus on testing, documentation, making sure that software will do what is expected.

I find this to be a mean and misguided post. To suggest that Victor Taelin does not know about formal methods. As I understand, he is trying to do something genuinely new and interesting. And he is transparent about his work, which he then gets hounded for. A shame.

> To be fair to Bend, I completely vibe-coded this, I just told a LLM to recreate the demo in SPARK

A vibe-coded retort to a vibe-coding tool? Ugh.

Very off-topic, but the 'humans write “laws”' phrasing made me think of using LLMs to unit test real laws. Have them come up with test cases to see if the phrasing is as intended or has loopholes. Wonder if anyone's tried doing something like this (probably not, I imagine this is too much tech for government)

All I see from this article and the whole saga is pure sadness. The situation seems unfortunate but seemingly unavoidable.

I think they know the standards of formal verification. They just surf the AI hype, whip up a verbose Python-like language that is worse than any existing prover language and have 20k bots star it.

This is the way to succeed these days.

The code itself is the most compact representation of the rules you want applied.

The vibe coding dunning krueger damage has yet to surface, but I'm guessing it will be in the billions. I'm not even talking about the insane infrastructure investments - thousands of c suite execs are vibe coding pointless crap instead of delegating it to their team that knows what they are doing, wasting thousands on tokens if they are on enterprise API plans for zero return or spending 30$ on creating an interactive html page for stuff that should be a power point slide with a few bullet points. It's totally insane!

> Feel free to replace “the author” below with “a hypothetical author who could have created the same thing”.

This is honestly sleazy, just admit you were basically way off.

@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?

It seems like this is largely a matter of what you’re asking for. If you wanted to do more research into the state of the field, an AI might be pretty good at answering your questions.

what a horrible blog-post :( Bend, HVM, Interaction Combinators, etc. isn't some vibe-coded fantasy, and the author has been working on this stuff for a loooong time.

how incredibly disrespectful :/

"If you ask a LLM for a language where it’s possible to prove that a function is formally correct by building up a proof from basic principles then it will happily do so, it will never stop to suggest to you that computers can already build complex proofs without the need for a LLM and eliminate 99% of the work. It will never tell you that what you’re building already mostly exists as work that you can build on."

I don't know what llm you use but current llms will definitely let you know about similar things out there. So this statement is a bit incorrect.

I wouldn't use SPARK either, and rather develop my own approach. The problem isn't that the proof has 400 lines of code, every modern system has large proofs (Isabelle/HOL, Lean, etc.) My latest formal proof has over 50K lines of proof. That's why AI is such a useful tool.

It absolutely drives me up the wall when I hear someone wrote their own language or framework because "the current ones just didn't do what I wanted to do" and then the result is a worse language/framework that the LLM and person know.

I absolutely endorse new creations when they are necessary but the people making these aren't doing it from a point of education, they are doing it purely because _they_ don't understand the framework or language that is the standard for that area.

It always always always involves a high level of AI Psychosis, that a brand new web framework is needed for your revolutionary... CRUD app?

Pro: it can be an excellent way to learn if you realize good problems don't come easy, many such cases where I abandon something having learned from it and that's life

Con: the machine will tell you you have easily found a good problem, and engineered the perfect and necessary solution, if you let it

"Know what to ask for" is what will keep me with a job for a while longer, I guess.

A language for LLMs will never be a compiled language. The best language for LLMs would be something that can be interacted with. Like a Lisp.

As a resident of Bend, Oregon, checking the homepage sets off some kind of "oh look, Bend!" alarm in my brain.

If employer doesn't care about substantail 442 line fix, why should I?

This whole article can basically be summarized as "why is anybody building anything that already exists" gatekeeping.

Despite the fact that the entire premise is incorrect since the author of the language clearly has been shown to know about formal verification, this is basically encouraging nobody to ever post anything they work on for fear it might be "similar" to something already out there.

Is this really where we want the industry to go to all because of vibe coding?

The author of the article itself also clearly did 0 research of their own at all on the author of the language, and admits to vibe coding their own example themselves.

What the fuck are we doing.

> The problem is that vibe coding makes it possible to build a substantial solution before learning enough about the problem to recognise that a much better solution exists.

This is precious.

"This example matters beyond Bend, vibe-coding makes it makes it far too easy to implement a design that’s horribly broken or decades behind the current state of the art because you can immediately get a result without ever having to do any research."

This is totally true but almost totally irrelevant. I'll use some hyperbole here to make the point: Whether the design is broken or decades behind doesn't matter anymore. Neither of those are an outcome/end goal. They are means we historically have used to achieve good end goals or outcomes.

In the end, the goal is usually "does it meet the needs of the person who needed it" not "is it good software". If it no longer meets their needs and they can vibe code another total piece of shit in an hour that meets their needs again, they still may be "better off" than spending time researching the field and learning and ...

This may feel shitty, and it may feel like it should not be true. But right now, that seems to be true?

In that sense, the author is wrong that vibe-coding is a trap. The trap is assuming you have to make something good to meet someone's needs both now, and in the future.

Now, like i said, this is hyperbole, and there are lots of good arguments against it. The author's just isn't one.

Technically good or better has never mattered very much in the marketplace, despite people wanting it to really badly (ease of use often mattered, but not technical goodness). Software engineers often took pride in their work and so there were usually kernels of goodness in even the shittiest software. All you are seeing is that now it is nowhere near as hard to create and bring these "solutions" to market, and more importantly, doesn't necessarily require anyone who has any pride in their work at all, or even have any experience in software engineering. As such, technical goodness has mostly gone out the window because the market never required or really rewarded it.

Yes I think fundamentally the effort required to understand, write, and verify a formal specification is just way higher than is reasonable in most situations.

There are some cases where it is pleasingly simple - usually low level algorithms like compression, sorting, search etc. Basically things you'd find in leetcode questions.

Most software isn't like that.

I think the actual answer is just that the very latest models (e.g. Astra) are actually quite good at writing normal tests, and you can just skim them to make sure they're doing something sane.

The problem is that vibe coding makes it possible to build a substantial solution before learning enough about the problem to recognise that a much better solution exists.

We need a catchy name for this phenomenon.

I feel like this is the same black hole as small local models.

Things people want to be awesome and true, and things that are actually awesome and true don't intersect the way people want them to.

…so if there was an easy way to do provably correct AI code, it would be nice.

…but I’d also like a frontier that runs on my raspberry pi and a cheap fully autonomous self driving car that just uses a single cell phone camera.

Unfortunately wanting those doesn't make them exist; and people telling you they do exist usually are either a) uninformed, or b) selling something.

Finally a bit of sense in this madness.

This tells way more about you than Taelin. You didn't take a minute to research about Taelin, his past work, his company, and the design decisions behind the language. FFS, why people are like this.

>Bend just serves as a useful example of my general point regarding vibe-coding as it is recent, high-profile, and has aspects that make it easy to use as an example. I don’t know anything about the author’s history with designing languages or if they actually did consider the tradeoffs below and made what I think is a poor choice

This doesn't make any sense, you're equivocating vibecoded as in "prompted by a clueless incompetent person" with vibecoded as in "implemented by an LLM". Former is used to make your point, later is used to defend the premise.