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)

I'm assuming you have not spent a lot of time trying to prove stuff about non trivial programs if the trade offs between SMT based approaches and interactive theorem provers are not clear to you.

SMT solvers are highly automated, but very opaque and hard to debug. Interactive theorem provers can scale to larger problems and harder properties at the cost of increased manual proof burden. The ever increasing ability of llms to write proofs in a theorem prover has in recent years tipped the balance significantly towards preferring itp based approaches over pure SMT ones. The current state of the art for program verification is probably a mix of llm and traditional (tactics, SMT, etc.) proof automation inside an itp.

If you're going to insinuate that the author of Bend2 doesn't understand PLs and formal verification, you should do so with some proof and not a hot take dunk.

I think it's fine to critique the language and the approach without criticizing the author and I hate that this site has become Tech Drama News, like the worst parts of Twitter.

You clearly don't know shit about the whole topic, yet attack an open-source project's author who wasn't even the one posting his own project..

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

Because code is trivially cheap now. LLMs churn out a shitton of code at pennies, and as technology improves their per-line cost will continue to decrease. A proof has to be written once and it's never read again. It's only important property is that it is machine-verifiable - from then on only the signature matters. Meanwhile speed of compilation matters, so an obvious tradeoff was made by the author.

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

This is clearly not the case here, and even if it were, it's still a better thing than vibe-blogging clickbait shit with extra amount of Dunning–Kruger. Calling out an author who clearly works in the field for a decade or more for not knowing the topic...