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

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.

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.

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