> 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.
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..
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.
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.
LiamPowell · · focus · HN ↗
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 · · focus · HN ↗
>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.