> 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.
Back in 2018 they were working on Formality, an Ethereum formal verification project. They are the Victor in this video about it: <a href="https://slideslive.com/38911748/introducing-formality" rel="nofollow">https://slideslive.com/38911748/introducing-formality
Here's the GitHub repo for that, which demonstrates familiarity with formal proofs that long predates LLMs <a href="https://github.com/VictorTaelin/Formality" rel="nofollow">https://github.com/VictorTaelin/Formality
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:
<a href="https://news.ycombinator.com/item?id=49753898">https://news.ycombinator.com/item?id=49753898
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
z7 · · focus · HN ↗
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 · · focus · HN ↗
Here's the GitHub repo for that, which demonstrates familiarity with formal proofs that long predates LLMs <a href="https://github.com/VictorTaelin/Formality" rel="nofollow">https://github.com/VictorTaelin/Formality
LightMachine · · focus · HN ↗
sighs
Here's my response to this ridiculous accusation: <a href="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 · · focus · HN ↗
verdverm · · focus · HN ↗
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