Bend 2 and the Vibe-Coding Trap

> 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 and we will 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 all our collective input, thoughts, human 'thinking traces' they collect in their meta-data as their 'innovations' any more.

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.

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

> 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 made my first half-dozen DSLs in the last couple of years with the assistance of these tools. Each one taught me valuable lessons about a whole gamut of considerations, from architecture to semantics and to all of the DAPs and LSPs between. Let it be known that the early approaches were, erhm, not very good.

"What if it did this..." and being able to quickly iterate is a fantastic way to explore the surface area of a new programming language.

This being said, I am past sharing these projects on this site as it really draws out an uncharitable crowd.

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?

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.

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

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.

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

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

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

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.