235 comments
This example and Bend aside, I find this to be the biggest struggle with the perceived intelligence we have today. It's great at producing something that works, but it is not great at calling you out when you don't know what you don't know.
It's not able to educate and course correct you unless you have great self awareness and discipline.
That said, I think this goes for everything, it's easy to fall into this trap because it is very human. We simply don't know what we don't know, so it's not uncommon to revisit an old solution only to be enlightened that there is now new information that allows you to replace it with something much better.
I don't think anything here is new or changed, if anything changed is really just the rate that we experience this. LLMs make it easier and faster for the feedback cycle to happen.
Now back to Bend, I think putting your work out there and being unapologetic about it, open source even, and willing to take feedback, will go a long way.
I am more worried about the many closed source implementations of LLM built products that are being sold and people are depending upon that don't get this great criticism from many different thinking heads.
> I don't think anything here is new or changed
I would argue it's a little new though. I used to write dumb little programs all the time that explored an idea which was probably bad, and in that exploration I often found that there was a better way to do it, or that I didn't know as much as I thought I did, or that another thing already existed that was much better considered than my half baked idea, etc. But there was learning that happened there, so the process was still valuable. Now you can get a working bad idea without learning anything, there is full conservation of ignorance, but a full dopamine hit from "i made this thing". I guess you could argue it's just everything happening at a faster rate, but it feels different to me, and it is pretty eerie.
Before you would pause at overwhelming, now you get to "fail forward" with less at stake because the end result can still be verifiable even if the internals are a blackbox to you.
It's a sort of "deferred" and/or "optional" learning dilemma we now exist.
You could open the box, look inside, ask questions, but you would need to care and feel engaged, which is very hard to do when the result is already there.
This is why I framed it as requiring self awareness and discipline. Very easy to get caught into the slot machine dopamine cycle loop.
or itself, the moment it hits some ambiguity it becomes a spaghetti throwing machine, half the time using a single attempt (arbitrarily picks answers with little logic or attention to nuance).
They've been trained to behave in ways that make them run longer, quantity over quality. I suspect this is because the people training them are extreme vine coders. Certainly seems that way by their public statements and harness releases.
I would much prefer if they stopped and asked questions. Mild improvement with markdown engineering...
Developers intuitively know that the development process would inevitably yield learnings that would shape and change what the final product could and should be, while managers typically dismiss this in favour of an illusion of productivity.
Not even the demo on that release works well.
I received several very emotionally charged responses centered in the personal credentials of the author. They felt very out of place and did not engage substantively with any of the things I said. It was indeed very weird
The author, who I hadn't heard of before yesterday, actually seems like a cool dude. He was quite responsive, normal, and engaged with my feedback, which makes other random accounts being offended on his behalf all the more uncanny
Your post and the ones that followed are a good example of the contrarian dynamic that dang often talks about. https://hn.algolia.com/?dateRange=all&page=0&prefix=true&que...
I took a look and honestly the replies were a lot more reasonable than I was expecting them to be. I don't think it's that out of place for people to inform you that the author has been in this space for some time and has prior work to look at (pre-vibe coding era). Really there was one reply citing his prior work, you responded to it calling it a very strange reply and were "very confused" why they would point to his history, even though you had just said things like:
>I'm glad you're having fun vibecoding, and I like that you're interested in this area of research/engineering
To me, it makes sense why someone would say the author has been interested in this area for a long time and pointed you to some prior work that was not vibe-coded, given your comment strongly implies they are just messing around and don't know much about the field.
To be clear, I share much of your feelings in your original comment. I just felt the replies weren't so unreasonable either. At least, I was expecting them to be a lot worse.
"I'm glad you're having fun vibecoding" comes across as very backhanded and condescending. It sounds like you may have actually meant that genuinely, but it doesn't read that way in text form.
"you sound sus af" is not respectful or constructive in my opinion. It's a description of your own feelings, not a critique of the project, and there's not really any way for the author to respond besides ignoring it or saying "sorry you feel that way" or something.
I think that line undermines the rest of your comment, because I'm left thinking that you don't really expect good answers to your questions and you just think the whole thing is dumb.
If I have years of experience on the topic and invested significant time into the project, I'd not be as civil as the author if someone came in and essentially called it vibecoded slop.
There is nothing weird about how others pointed out that the project appears to have merit contrary to how it at first might have looked to you.
[0] https://news.ycombinator.com/item?id=40390287
Lean4 itself has 9k
Also, wrote a response to this whole thread here:
I would rather wait to see how it gets adopted, if at all. Anyone aware of early reviews of the adopters of bend 2?
Invariants were like "if outside temp < 40 or inside temp < 65: heater.minTemp( 65 )"
Axioms were like: "if {we're home} and it's {not a holiday} the house should be {comfortable temperature}".prompt
...and then that would get decomposed and translated into interlocking code for the scene(s). I'll have to look at this language a little more closely with those kinds of constraints in mind!
You're kindof translating `*.prompt` to either prolog (yucky!), lisp, lua, or javascript (for inspectability/debuggability), but this whole bend thing might be an exact fit for the problem space! Limited set of objects and states, bounded set of "invariants" (laws), and layering on top the general state modification activities (either "evaluated every 5 minutes and reconciled" or "set the scene xyz...").
>vibe-coded project
many such cases
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
I am glad I saw it, as now I am interested in learning more about Bend.
GNATprove uses SMT solvers, meaning it's basically a brute force proof system.
Yes, brute-force proofs are easier than symbolic proofs (lean, bend, etc.) because you don't have to supply a proof. It's all automatic.
But brute-force proofs don't scale to nearly anything of interest, which is why formal verification has been a niche field for 30 years, until now where LLM can write _actual_ proofs.
Read the full thread on Hacker News →
Related stories
- DEV Community · 18 points · 5 days ago
- DEV Community · 0 points · 2 days ago
- Hacker News · 2 points · 10 days ago
- Vibe Coding Developer Productivity Toolsmikemcquaid.comHacker News · 2 points · 4 days ago
- Show HN: I am vibe coding a droneai-eng-design-production.up.railway.appHacker News · 5 points · 11 days ago
- The Dangers of Vibe Codingthesimpledev.comHacker News · 2 points · 9 days ago