Posted by LiamPowell 5 days ago
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.
I also would argue that in this case, the end result wasn't good but rather perceived good. It was good enough to pass a smoke test, but not an integration test, and end-to-end test, a runtime edge case, etc.
All of software development lifecycle should still apply and be relevant here, the tool just changes the rate at how it gets written and it is tempting to move faster and continue skipping other steps. Especially so in greenfield work as a solo founder with limited time.
I think at the end of the day, a good metric is your "give a shit quotient". How much do you give a shit about what you are doing is likely the most important thing into how it is going to perform.
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.
How can we "course correct" with "self-awareness and discipline"?
Discipline would be turning this into principles you practice constantly, it's more of a lifestyle rather than a skill you "obtain".
For example, starting from the position of "I am taking on an idea where I may have knowledge gaps in" you first prompt for research and validation rather than execution. Even if the end result is you were right on your original design. (Sort of a challenge, adversarial, by default)
It will slow you down, but may lead to more sticky results.
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...
In my own professional life, I've found this to be a very divisive statement. For some, it is a sign of wasting time and effort. For others, they use this to describe themselves when they want to do exploration for the goal of finding improvements, without any clear goal because they have a few ideas but none worth putting forward. I've been told to spend time learning AI and have found that saying "Yeah, I'm playing around with it." was the wrong thing to say because it was seen as not doing anything worthwhile. It doesn't matter that I would also say the majority of my tech skills were developed when I was "playing around".
I wonder if this is purely a linguistics breakdown, or if this is tied to some deeper difference in a person's relationship to tech?
Ironically, people with this mindset will sometimes ask people who they recognize as having strong skills to share their magic secret, which is assumed to be some books they read, videos they watched, courses they attended, etc. If you tell them that experimenting, playing around, etc. is a key element, they may assume you're just selfishly hoarding your fount of knowledge.
I don’t see anything from your parent commenter on the other thread that deserves that classification. On the contrary, while they initially had suspicious of vibe coding, on later comments they are cordial and even admit their own misunderstanding.
What am I missing? Where does “called him suspicious as fuck” come from?
Edit: Answered below (https://news.ycombinator.com/item?id=49754311). Thank you.
The whole "Wow, looks AI" > "Yeah, some of it is, we'll fix it later" was such a small part of the conversation, but then there are countless of other people chiming in about specifically the "Is It Slop Or Not?", rather than the meat of the conversation. And here we are adding even more meta-comments about it.
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 agree with the other poster that is was very suspicious initially (sus af is not how I would put it, that sounds like a generational term) the author nuked their commit history while simultaneously pointing to a (Fable-written) paper which referenced the commit history in benchmarks. Then they seemingly had no understanding of why that's trust-breaking.
So to me, it sounds like the author didn't even read the paper they wrote, because otherwise they'd have remembered referencing the commit history, and wouldn't be asking us why we'd even care about it. “They” told us care! I'm glad they restored it but apparently that wouldn't have happened without the criticism.
What I didn’t understand when expressing confusion with the responses, and still don’t, is the personal nature of the response. It wasn’t pushing back against anything I said really, moreso it tried to bring up the credentials of the speaker; and, I guess this feels a nonsequitr
Like, if I say “I have these problems with thing X”, it doesn’t really matter who made X. Sure, it’s context I didn’t have and there is something to be gained in saying it; but, it doesn’t really change any of the critiques I had. Appealing to the authority of the creator doesn’t engage with nearly everything I said
How is that a non-sequitur? You're the one who brought up the topic of credibility in the first place. The comment was simply made in response to that.
"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.
I was writing the comment very stream of consciousness and not really think about how it may come across
If I were trying to boil down what I’m attempting to communicate, it would be 1. The project seems cool, but it’s also making some very strong claims that I’m hesitant to accept
2. The coolness of the thing is undermined by the presentation of it. It comes across as putting the cart is put before the horse, and the overly strong claims and marketing speak read as trying to rhetorically sway the audience rather than engage with them technically.
3. I genuinely am happy that the creator made this, but modulo the above worries I think it should be reeled in a bit. In part because of the concerns I have about the content, and further because it is the kind of language that I expect others to have a strong averse reaction to. Possibly to the point of also reaching the top of HN with their negative response
To a friend, it might be easy to capture some of this message with “you sounds sus af”, but to a stranger in the internet I see how I just sound like a jerk. Words do matter, and I think I’ll be more careful about this in the future
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.
If this is your first HN account and you haven't seen the site in the prior decade, the "emotionally charged responses centered in the personal credentials of the author" is the SOP. The site has yielded to that attitude because dang never enforced a sensible code of conduct, and relies mostly on favoritism and in-groups. Who says is more important than what is said, and the critiques you give are ranked according to whom you are critical of.
Think of this as a propaganda channel of a VC startup incubator who is brazenly looking for a product-market fit for anything and everything AI. Look at the roster of the recent startups and how many are AI-focused. Adjust expectations from there.
But I guess I totally ignored the YC context in that interpretation
[0] https://news.ycombinator.com/item?id=40390287
> They just recycled the Bend1 repo for Bend2 even though it's a completely different language.
Why would you kill the source history of Bend1 completely if it has 20K stars? You can only do that if Bend1 has no users at all right?
Does that meant that Bend1 isn't actually successful in its own right but rather only as a marketing project?
I wasn't one of the suspicious people but I am now.
I don't think that means it was "unsuccessful" in the sense you imply, though, because the project was never meant to be used in production. It was there to display a milestone (running inets on the GPU) and I was very clear it wasn't ready to be used yet. For example, it had only 24-bit integers, a 2 GB memory cap, and other limitations that made it unpractical. I still don't know why it has so many stars. I posted it to hacker news and that just happened. I guess it just went viral without really being ready yet, which got us to where we are now.
Anyway the commit history is back now. I apologize for nuking it
I say this as literally the first HN comment to call them out on this.
the author here is providing commentary on the vibe coding era, bend is just one example of people having ai build things for them they don't understand or haven't researched sufficiently, at least start with a vibe-search skill before the vibe-coding begins
Ai is only good at a task when the human driver is good at that task, and this is far more narrow than most realize. Someone who knows how to program will still fail on many programming tasks with agents, the field has far too much for any one person to know.
No one uses it seriously, and the author since then reverted the nuking of the git history.
Lean4 itself has 9k
I can unequivocally claim that Victor receives at least two orders of magnitude more social media engagement, while Lean likely has 4-5 more magnitudes of actual users.
Serious users of Lean simply have no need or reason to star the repository.
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...").
By the time your first round of beta testing is over, you may have quite a handful of such axioms and variants, which have been humanly validated!
Have you done any such experiment in this space?
Then break plain language requests into tool-calling-ish shared functions [atHome(), isHoliday(), comfyTemp(), ...] and basically throw "linker errors" if a concept didn't have a definition, eg: "ERROR: concept 'comfortable temperature' not defined..."
...and yes: be able to highlight overlaps or conflicting instructions at the semantic layer... those being less important than conflicts at the safety/invariant layer.
The idea was to have a bunch of basically "is_comfy_temp.prompt" => "is_comfy_temp.lisp" and be able to right click on any of the prompts and "show source" to understand, debug, simulate, validate, etc.
As you get real trials you end up with a foundational "StdLib" of at least necessary concepts although yours and mine might contain different data/preferences. And being able to edit "comfyTemp()" in one place as opposed to spread out in a bunch of different home automations (eg: isSummer vs isWinter else also: ifHumidity && upcomingWeather || realtimeElectricRates, etc...)
>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
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
I am glad I saw it, as now I am interested in learning more about Bend.
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..
>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.
> 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
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.
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.
> This example matters beyond Bend, vibe-coding makes it makes it far too easy to implement a design that’s horribly broken or decades behind the current state of the art because you can immediately get a result without ever having to do any research. If you ask a LLM for a language where it’s possible to prove that a function is formally correct by building up a proof from basic principles then it will happily do so, it will never stop to suggest to you that computers can already build complex proofs without the need for a LLM and eliminate 99% of the work. It will never tell you that what you’re building already mostly exists as work that you can build on.
---
That's why all your LLM requests to build something substantial should start with "run prior work research first". Of course, at some point everything converges (if we share our outputs open-source) and then we may have solid standard patterns and libraries and do not need to waste trillions of tokens globally to rebuild the same minor, fundamental things, each one in their silent little silo.
IF we share, it will be of course to the monetary detriment of LLM providers who will have less income overall, and of course now they can't repackage anymore all our collective input, thoughts, human 'thinking traces' that they collect in their meta-data, as their new 'innovations' any more to inflate IPOs / stock prices.
The searches it runs, and the summaries it provides, are all incredibly sensitive to your choice of words. Words you chose from a state of minimal knowledge. So it’s like a particularly perverse version of the anchoring bias: information that could have led you to a better solution is often actively filtered out of the agent’s response precisely because it leads down a different path from your first idea.
In short, if you ask an agent what’s the best hammer for driving screws, it’s liable not to mention that screwdrivers exist.
And yes the output of these researchers are highly sensitive to prompting. Left to their own devices the LLM will often ship some very biased prompts to its deep research agents loaded with pre-conceived ideas rather than letting the agents uncover things themselves. Then all the agents do is confirm what the prompt told them to rather then “think independently”. (Very similar to open ended interview questions rather than asking yes/no questions)
It’s is far better to spend a session writing writing the research prompt itself.
All of this takes time and tokens of course…
As in, are you sure, and can you provide concrete examples?
Yes, but I think there are incentives to not do this for many LLM providers. Doing prior-work research is slow (web searches aren't fast, LLMs are rate-limited or blocked from plenty of pages, etc.), and sometimes contradictory which annoys LLM users, many of whom like faster gratification cycles from the agent slot machine handle.
Also, writing a bunch of bespoke code instead of leveraging prior art makes a lot of users feel like they own something novel/big/important, and also poses a larger maintenance surface for the LLM to make future changes (which costs tokens).
I don't think there's, like, a conspiracy at LLM providers to set up system prompts/RAG/etc. to discourage research-and-use-prior-art-by-default approaches. Rather, OpenAI/Anthropic/Google/etc. are optimizing for real but sometimes misleading success metrics which often lead away from a research-first approach.
- But that shouldn't be confused with getting the LLMs to make the decisions. I believe that would quickly ruin a good design, unless the decisions are about truly inconsequential aspects, which are very rare in language and API design.
- I don't believe that (sharing) is to the detriment of LLM providers either. Not realistically. We would build faster and the questions / research directed at LLMs would be more sophisticated. Believe it or not, they can't cache questions as easily as websearch queries. If anything, I believe the more people learn to use LLMs effectively (rather than just to generate slop), the more their usage will be ingrained in daily life. Some of that will be redirected towards current LLM providers. But perhaps more of the economic share will increasingly go to hardware providers, as more and more people will be interested to run their own models.
As effective as “make no mistakes.”
It is trying to please you, and it always determines that the way to please you is to fulfill the original, core request. Any caveats or first steps will always be secondary to the ultimate goal of “this person wants to do X, so I will do X.”
The only first step I have found somewhat consistently useful, because as we know LLMs do not behave consistently, is when doing tech troubleshooting I will go “look at documentation for X before answering” so that it will search manuals and such. Helps avoid speculation. But even then, it’s still not full proof.
Sidebar: this is one of the core problems of LLM’s currently. You are basically arguing with them to get them to behave a certain way all the time and it’s not always clear if they’re doing what they’re being told to do. Then add the compounding layer that the longer the conversation goes on, the more likely it is to misunderstand or just ignore things as it descends into context-length-induced madness
Those aren't comparable instructions. Providing useful, related context to improve outcomes is a basic best practice, and asking LLMs to do research first is an important source of that.
I just want to be able to write C#, JavaScript or whatever, and then tack on preconditions, checks and so on with the same syntax. Dependent typing and design by contract for the masses.
Of course not, that would be equivalent to solving the halting problem, many people will say.
I wonder if that will change now: I'm happy with an imperfect sanitizer that I run every now and then and will run a couple of minutes and come back with: I've proved your conditions, I proved a violation, or I can't decide, please change your code.
Lean can be used as a regular programming language. There's also languages like idris2 and f-star, but they don't seem to have much traction.
Also, most of them are made to prove stuff first and foremost and thus trade off a lot of performance to the point that it makes them practically unusable for many stuff (e.g. numbers may be represented as an object that has n-1 further children recursively), though Lean is an exception as you note.
I don't think this is a big deal for day-to-day programming. You're trying to stay in n, nlogn or maybe n^2 realm most of the time. And the kind of infinite loops you encounter (e.g. event loops) are co-inductive or have some notion of making progress.
This is just about vibe-coded programs in general when the approach assumed by the article is taken. For all I know they did make an informed decision regarding the tradeoffs (which I would consider to be a poor decision).
> I just want to be able to write C#, JavaScript or whatever, and then tack on preconditions, checks and so on with the same syntax.
That's more or less what SPARK (and others) do, although specifications for large programs can become nasty.
> - The compiler (not kernel) is 99% AI-written and has not been fully audited yet.
> - Strings are linked lists of characters, so text processing is slow.
We will introducing binary buffers eventually. The project is new...
Now if you’re asking why the basic prelude String type remains as it is, that’s because changing it would break more code than it’s worth, at least as far as prelude’s maintainers are concerned. This is no different from how standard C strings remain a null-terminated sequence of bytes even though that’s been awful for everyday use for at least 30 years.
That said, yes, we definitely should have a compact Text type. I'll add it over the weekend.
https://www.usenix.org/system/files/conference/hotos15/hotos...
We survey measurements of data-parallel systems recently reported in SOSP and OSDI, and find that many systems have either a surprisingly large COST, often hundreds of cores, or simply underperform one thread for all of their reported configurations.Anecdotally I have a bit of a track record of 10xing slow systems’ throughout by converting them from distributed to single-node or from multithreaded to single threaded.
Heck I once even sped up a number crunching operation by getting it off of the GPU and onto the vector coprocessor. Because GPUs also have a bunch of extra overhead to have to amortize away.
You can slice up arrays in O(1).
The default type is incredibly clear to me.
so vibecoded
So what is the unique idea here except a vibe coded compiler that generates C and everything else is handled by clang+llvm?
From README.md:
>The compiler (not kernel) is 99% AI-written and has not been fully audited yet.
Also, why the compiler is not written against and with LAWS.md so that no audit is required at all?
There is a key difference: the laws are formally verified, as in Lean or Rocq (but much faster). So it's like writing a unit test or property-based test, but when it passes, you have a mathematical proof that you will get the expected output given ANY input in the infinite space of possible inputs. In traditional TDD, you make up some test case, write some asserts, and it passes if you get the expected outputs from those inputs and only those inputs. So you have to make multiple test cases for the same thing, and you still don't have any formal guarantee of your code's correctness.
> Also, why the compiler is not written against and with LAWS.md so that no audit is required at all?
Because it is mathematically impossible due to to Gödel’s second incompleteness theorem, which states: any consistent formal mathematical system strong enough to harbor basic arithmetic cannot prove its own consistency
A little research before writing and publishing a personal attack like this could have substantially improved the result because the author would have known what they're writing about
Victor is not a formal verification noob as this article suggests