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

▲

f0e4c2f7 4 hours ago | parent | next [-]

It's amusing to me this entire article is centered around brow beating this and other hypothetical software authors for starting things without doing a small amount of research first to understand the very basics of what they're getting into.

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.

▲

simonw 5 hours ago | parent | prev | next [-]

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

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

▲

LightMachine 3 hours ago | parent [-]

Victor here. I haven't "worked" on Formality. I've founded it. Designed every part of it. Before LLMs!

sighs

Here's my response to this ridiculous accusation: https://news.ycombinator.com/item?id=49753898

I can't internet anymore. I need a beach

▲

N_Lens 3 hours ago | parent [-]

Sympathize with you mate, this article just seems like a poorly researched hit job.

	▲	verdverm an hour ago \| parent [-]
		The article is about vibe coding, bend is the main character because it made frontpage. The author here says as much in the introduction, that it is not about whomever is behind bend, but the larger trend The author here has also added bend's author's link (in GP) to the original post, they very much do not seem to be doing a "hit job" and their intent is to comment on patterns from vibe coding

▲

mannykannot 4 hours ago | parent | prev | next [-]

Bend's developer has posted a well-argued response here: https://news.ycombinator.com/item?id=49753898

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

▲

crvdgc an hour ago | parent | prev | next [-]

To be fair, if the two words indeed don't appear in either the webpage or the codebase, it is a bit strange. It's like implementing a whole Google alternative without ever using the words "search engine".

▲

ahknight 3 hours ago | parent | prev | next [-]

He claimed the guy did no research while himself doing no research? I'm shocked! Shocked! Well, not that shocked.

▲

LiamPowell 4 hours ago | parent | prev [-]

I don't want to change that sentence now that people have discussed it, but I have added a note to the top to make it clear that I'm just taking it as an example of a vibe-coded program because it's recent and high profile.

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

▲

littleroot 10 minutes ago | parent | next [-]

>I don't want to change that sentence

>but I have added a note to the top

you know what's the least you could actually have done instead? no, you don't need to retract the blog post at all, keeping it up was the right choice. Now slap a big ass apology for being an unaware snob on top of it instead of leaving a link to the author's reply, like an after thought.

▲

killerstorm 3 hours ago | parent | prev | next [-]

> Look like how AI slop has unrealistic physics

> Posts a link to real moon landing footage

I'd delete the article if I was you...

You know, in academia, they sometimes retract articles, even if they believe they are directionally correct

▲

LiamPowell 2 hours ago | parent [-]

I feel that that's the worst option because it only leaves people who have read it without the added context at the start. If someone convinces me that I'm wrong then I'm happy to do so though.

	▲	gf000 an hour ago \| parent [-]
		You should add a strikethrough to your post and post a public apology to the author.

▲

jibal 4 hours ago | parent | prev [-]

> I'm just taking it as an example

But this is grossly intellectually dishonest. You know very well how this will be read and responded to here ... and you keep saying that you're just talking about vibe-coding oh but you have serious criticisms of the specific effort. You write passive-aggressive stuff like

> For all I know they did make an informed decision regarding the tradeoffs (which I would consider to be a poor decision).

which contradicts your base assertion that their decisions were not informed. And

> My critiques of the language itself are not the main point, although I do still think that it's a very bad design ...

You claim

> The developer has built an entire language around a field seemingly without realising that said field exists.

but that is severely factually wrong, which along with a lot else suggests that you have very bad judgment. As the author writes,

> Bend proofs being verbose has nothing to do with me not knowing that inference, unification, or program search exists.

IOW, you have made a serious error in logic.

> To be fair to Bend, I completely vibe-coded this

Some advice: DBAD

You trashed the author and his work without bothering to learn anything about either one first (which is quite ironic).

I won't respond further.