YHK - yet another hacker news clone

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

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.

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?

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

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

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

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

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

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.

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

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.

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.

Finally a bit of sense in this madness.

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.

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.

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

"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. 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 type-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 proof 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. It is an intentional choice I made after considering every alternative.

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