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.

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.

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.

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

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

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

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

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.

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

We need a catchy name for this phenomenon.

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?

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

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 the way to succeed these days.

If the author of the article had done just a small amount of research about bend or it's author before writing the article they would have known pretty quickly what they were saying was incorrect.

I think the larger pattern here is that nuance is one of the most valuable commodities in the AI era. If you're hand waving stuff away without even missing , you're going to miss a lot of stuff in this cycle.

This article reminds me a lot of the famous hacker news Dropbox comment.

Here's the GitHub repo for that, which demonstrates familiarity with formal proofs that long predates LLMs https://github.com/VictorTaelin/Formality

I am glad I saw it, as now I am interested in learning more about Bend.

My critiques of the language itself are not the main point, although I do still think that it's a very bad design to have a LLM waste tokens on a proof that could be written by CVC etc..

The searches it runs, and the summaries it provides, are all incredibly sensitive to your choice of words. Words you chose from a state of minimal knowledge. So it’s like a particularly perverse version of the anchoring bias: information that could have led you to a better solution is often actively filtered out of the agent’s response precisely because it leads down a different path from your first idea.

In short, if you ask an agent what’s the best hammer for driving screws, it’s liable not to mention that screwdrivers exist.

Yes, but I think there are incentives to not do this for many LLM providers. Doing prior-work research is slow (web searches aren't fast, LLMs are rate-limited or blocked from plenty of pages, etc.), and sometimes contradictory which annoys LLM users, many of whom like faster gratification cycles from the agent slot machine handle.

Also, writing a bunch of bespoke code instead of leveraging prior art makes a lot of users feel like they own something novel/big/important, and also poses a larger maintenance surface for the LLM to make future changes (which costs tokens).

I don't think there's, like, a conspiracy at LLM providers to set up system prompts/RAG/etc. to discourage research-and-use-prior-art-by-default approaches. Rather, OpenAI/Anthropic/Google/etc. are optimizing for real but sometimes misleading success metrics which often lead away from a research-first approach.

- But that shouldn't be confused with getting the LLMs to make the decisions. I believe that would quickly ruin a good design, unless the decisions are about truly inconsequential aspects, which are very rare in language and API design.

- I don't believe that (sharing) is to the detriment of LLM providers either. Not realistically. We would build faster and the questions / research directed at LLMs would be more sophisticated. Believe it or not, they can't cache questions as easily as websearch queries. If anything, I believe the more people learn to use LLMs effectively (rather than just to generate slop), the more their usage will be ingrained in daily life. Some of that will be redirected towards current LLM providers. But perhaps more of the economic share will increasingly go to hardware providers, as more and more people will be interested to run their own models.

As effective as “make no mistakes.”

It is trying to please you, and it always determines that the way to please you is to fulfill the original, core request. Any caveats or first steps will always be secondary to the ultimate goal of “this person wants to do X, so I will do X.”

The only first step I have found somewhat consistently useful, because as we know LLMs do not behave consistently, is when doing tech troubleshooting I will go “look at documentation for X before answering” so that it will search manuals and such. Helps avoid speculation. But even then, it’s still not full proof.

Sidebar: this is one of the core problems of LLM’s currently. You are basically arguing with them to get them to behave a certain way all the time and it’s not always clear if they’re doing what they’re being told to do. Then add the compounding layer that the longer the conversation goes on, the more likely it is to misunderstand or just ignore things as it descends into context-length-induced madness

I'm just leaving you a comment to counter the influx of negativity coming towards you for no reason.

I hope you are doing well and won't take all this too badly -- try to think of it as just free marketing for your project!

Have a nice day!

Sorry. See the edit at the top if you haven't already. I didn't realise how much it came off as a critique of you rather than a particular approach to software engineering.

It's easy to write something and have a model of what you're writing in your head that is massively different from how someone else will read it without realising, not that that excuses it.

---

I disagree with LLMs manually writing proofs without other tools doing all the work they possibly can ever being a good solution for a couple of reasons:

1. Tokens are really expensive when we have a LLM spending hours hacking aware at a proof, not to mention generating those tokens is slow.

2. The context window becomes flooded with proof work rather than work on the original problem, which will lead to a worse solution. LLMs are demonstrably worse at writing code when you continue a session on a new task instead of starting a new one.

> It is my vision that a good proof language should be fully explicit, because this reduces proof-checking time significantly.

We can cache the results and help the checker along with assertions rather than throwing out all the smart parts of the checker.

Do you have benchmarks which show this?

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.