3 ms·

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

by z7 15d ago

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

simonw 15d ago
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 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 https://github.com/VictorTaelin/Formality
- LightMachine 15d ago
  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 https://news.ycombinator.com/item?id=49753898 I can't internet anymore. I need a beach
  - N_Lens 15d ago
    Sympathize with you mate, this article just seems like a poorly researched hit job.
    - verdverm 15d ago
      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
LiamPowell 15d ago
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..
- jibal 15d ago
  > 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.
- killerstorm 15d ago
  > 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 15d ago
    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.
mannykannot 15d ago
Bend's developer has posted a well-argued response here: https://news.ycombinator.com/item?id=49753898 https://news.ycombinator.com/item?id=49753898 I am glad I saw it, as now I am interested in learning more about Bend.
f0e4c2f7 15d ago
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.
ahknight 15d ago
He claimed the guy did no research while himself doing no research? I'm shocked! Shocked! Well, not that shocked.
crvdgc 15d ago
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".

by z7 15d ago

simonw 15d ago

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 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 https://github.com/VictorTaelin/Formality

LightMachine 15d ago
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 https://news.ycombinator.com/item?id=49753898 I can't internet anymore. I need a beach
- N_Lens 15d ago
  Sympathize with you mate, this article just seems like a poorly researched hit job.
  - verdverm 15d ago
    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

LiamPowell 15d ago

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

jibal 15d ago
> 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.
killerstorm 15d ago
> 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 15d ago
  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.

mannykannot 15d ago

Bend's developer has posted a well-argued response here: https://news.ycombinator.com/item?id=49753898 https://news.ycombinator.com/item?id=49753898 I am glad I saw it, as now I am interested in learning more about Bend.

f0e4c2f7 15d ago

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.

ahknight 15d ago

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

crvdgc 15d ago

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