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

Because it should be smart. I mean, why would a human coder ever observe standard best practices unless the client specifically asks them to?

But it won't tell you if you don't ask. It won't tell you, "This approach is stupid, Ada SPARK exists".

The whole original conversation was very smelly from the very start, 20k stars included on the GitHub page with lost history.

We know what kind of turf that is.

I posted a sharp critique in the original discussion, aiming to be civil while critiquing the project. I may have been a bit terse, and would probably rephrase some of it now to avoid confusion, but I don't think I was ever outwardly disrespectful.

I received several very emotionally charged responses centered in the personal credentials of the author. They felt very out of place and did not engage substantively with any of the things I said. It was indeed very weird

The author, who I hadn't heard of before yesterday, actually seems like a cool dude. He was quite responsive, normal, and engaged with my feedback, which makes other random accounts being offended on his behalf all the more uncanny

Narrowly, I think you're spot on. The effort required to understand the machinery around formal verification is a function of the surface area of the thing being formally verified. Specifically, formally verifying the surface area of general purpose programming languages is difficult.

My approach with Hale (shameless self plug) is that the programming language itself first offers another strata of structure to program within, a type of graph. Once the structure of the program is expressed as a graph, understanding how formal verification works is a clean encapsulation of graph activities.

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.

This is probably not necessarily true. “f: list[1 A] -> list[A] pure, worst-case time n log n, such that for all x and 0 <= i <= j < len(x), f(x)[i] <= f(x)[j]” is probably good enough for nearly everyone unless the program synthesiser is actively adversarial; probably 99.999% of the list-sorting in the world is done via standard library functions anyway, which suggests that people don’t much care exactly how it happens.

Think you could argue that’s more LLM-assisted engineering than it is vibe coding.

It seems implicit in the article that the author should have remembered to ask, as part of the prior research.

Thanks. Read your update and I think this is an interesting conversation to have in the open.

Perhaps because their concerns are different? Similar reasoning: "why invest in dependently typed languages over SMT solvers? SMT solvers are automatic, and it is way easier to add annotations to my programs"

The answer is that these technologies are not universal in trade off space.

Of course, if you can have an LLM prove something by dispatch to an SMT solver ... you want to do that (and, indeed, LLMs do sometimes do this even when working on Lean proofs)

But the space of statements that you can prove using verification with SMT is smaller than dependently typed systems.

Also, Ada/SPARK are very good and robust -- they've been around for ~50 years ... but there's been a significant amount of work in formal verification since then, right? I would be more clear that Ada/SPARK are state-of-the-art for "mission critical software" (and have been for many years), but there's been a lot of research work in formal verification of low level programming since then (Low*, for instance)

Or maybe it should be a flag to indicate that there might be more to think about before handing the task of to an LLM.

"run prior work research first".

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

Humans dont let LLMs raw dog internet web searches.

That's why all your LLM requests to build something substantial should start with "run prior work research first".

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.

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.

Back in 2018 they were working on Formality, an Ethereum formal verification project. They are the Victor in this video about it: https://slideslive.com/38911748/introducing-formality

3 bend posts on the front page of HN. Astroturf