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.
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.
Here's the GitHub repo for that, which demonstrates familiarity with formal proofs that long predates LLMs https://github.com/VictorTaelin/Formality
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
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
I am glad I saw it, as now I am interested in learning more about Bend.
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..
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.
> 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
>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.