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.

Not even the demo on that release works well.

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.

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.

> 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.

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

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?

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

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.

The irony of this post talking about vibe coding and not doing one’s research, on only not have done even the slightest inkling of research themselves (heck, even asking an LLM about the author would for sure have turned something up).

I hope people will give it a second look, and not just stop at this post which is a gross misrepresentation of Victor Taelin’s work.

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.

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

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.

how incredibly disrespectful :/

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?

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

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

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 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.

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

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.

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?

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.

This is precious.

We need a catchy name for this phenomenon.

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.

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.

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.