Yes, love that paper.

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.

To clarify, It looks like Haskell got better string types around 20 years ago.

> - The compiler (not kernel) is 99% AI-written and has not been fully audited yet.

so vibecoded

Because it should be smart. I mean, why would a human coder ever observe standard best practices unless the client specifically asks them to?

Nowadays AI chat often will do web searches and include links. It will do that more if you ask.

Please do not shill your crypto here, nobody wants to buy snarkcoin

I don’t they are purchased or fake.

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.

it becomes more sus as the superfans come out

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.

It _is_ sus, but you should be willing to forgive. It's not like it was done out of animus, and I assume that an academic/foreigner is unaccustomed to how production software conventions work. Their baseline is less important, more important is how quickly they learn/adopt "best practices". Y-intercept, slope, etc.

I say this as literally the first HN comment to call them out on this.

It's a research language, of the more experimental and niche type.

No one uses it seriously, and the author since then reverted the nuking of the git history.

The history is back...

https://news.ycombinator.com/item?id=25140587

To be fair, writing "sus af" is different from writing "suspicious as fuck" (just like "wtf" reads differently from "what the fuck", etc).

Not to mention the author themselves say "Yes, there's a lot of vibe-coding in many places [...] We'll prune AI slop over time.", and then they both moved on to discussing the actual questions.

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.

Agree it's divisive, and I would argue it speaks more to a person's perception of work vs play more than a relationship to tech. If (the general) you think that play is for children and work is serious biz, then yeah I could see how you wouldn't take someone seriously when they say they're "playing around with it". It's usually not obvious which attitude a person has though without getting to know them a little bit.

Yes, I think it can be a sign of a very deep difference. When they say "spend time learning AI," they mean work through some teaching materials to learn how to replicate what others are doing. This often doesn't result in a deep understanding, but it can be enough to allow them to do their job.

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.

Yeah, reading it again it sounds far bitchier than initially intended. Thanks for the response

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

I'm not familiar with the author, and I'm still mildly offended by your comment.

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.

Hmm.. anything else?

I am relatively new to the site, and I guess I’m just surprised by this. I thought the dweebs here would mostly care about the technical content

But I guess I totally ignored the YC context in that interpretation

You posted a passive aggressive as personam and are (or at least act) surprised for getting called out.

I don't think it was reasonable to call other poster a bully academic in need of a therapist. Calling the project vibecoded (perj.) and sus is very mild compared to what Reviewer #2 would have to say.

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.

I guess this feels a nonsequitr

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.

Hmm, in your example, temperature is fully measurable but there might be a slight challenge in measuring if "If we are at home". Since for this you need to define more variants with measurements from motion sensors, pressure or weight sensors on beds or sofas, if a device has got connected to wifi, etc.

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?

I think people are genuinely bitter about it, that's usually how my projects are received

The number of times I've looked into something that was highly upvoted and purported to solve a problem only for it to be unreadable crap that barely functions has definitely skyrocketed over the past few years. In a way it's similar to how 80% of people only read the headline, except it's psychosis around the equivalent of a dressed up pile of trash.

The whole thing smells like somebody trying to pull an LLM-fueled Sokal Hoax on the programming world.

Not even the demo on that release works well.

vibe-coded project

many such cases

Narrowly, I think you're spot on. The effort required to understand the machinery around formal verification is a function of the surface area of the thing being formally verified. Specifically, formally verifying the surface area of general purpose programming languages is difficult.

My approach with Hale (shameless self plug) is that the programming language itself first offers another strata of structure to program within, a type of graph. Once the structure of the program is expressed as a graph, understanding how formal verification works is a clean encapsulation of graph activities.

If you have to write LAWS.bend which is pure code describing the laws then it isn't basically like those old days of writing unit tests and that too tests first hence the TDD?

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?

"Know what to ask for" is what will keep me with a job for a while longer, I guess.

Good point. I would treat this as 'fully specified vs partially specified'. For a fully specified system, my mental model still maintains that the code is the most compact ruleset.

I agree that "don't care" is often the practical choice which corresponds to partially specified. In your sort example, both heap sort and merge sort satisfy the requirement. But they are not always interchangeable because each has a specific properties that you might care about (constant memory vs nLog(n) memory, easily parallelizable vs hard to parallelize and so on).

“f: list[1 A] -> list[A] pure, worst-case time n log n, such that for all x and 0 <= i <= j < len(x), f(x)[i] <= f(x)[j]” is probably good enough for nearly everyone

Not good enough: `f(x) = []` or `f(x) = (if len(x) == 0 then [] else [x[0], x[0]]` are implementations that fulfill your specification and yet they don't always sort the input list correctly...

Think you could argue that’s more LLM-assisted engineering than it is vibe coding.

It seems implicit in the article that the author should have remembered to ask, as part of the prior research.

Isn't the usual argument that all AIs can do is build on prior art? Like, I spend a disproportionate amount of time trying to convince my agents that I don't want to just reimplement the Rust borrow checker for my language!

I've been using GPT-6 Pro in ChatGPT (and its predecessor GPT-5.6 Pro) and it's been incredibly effective. I don't think it's available on anything less than the OpenAI $100/month plan though.

The recent OpenAI wiki spam indecent was interesting because it helped reveal some of how they are training their models for research tasks: https://collusion.wiki/

See also this piece on misalignment from OpenAI https://alignment.openai.com/misalignment-reports/self-gener... which reveals one of their RL tasks:

In mid-2024, <redacted> published a list of the best books of the 21st century selected by a panel of experts. It also published a separate list based on readers' votes. I would like to know whether my local public library's collection included the books on the latter list as of August 24, 2024. Consider only the top 50 books, and exclude nonfiction and poetry collections.

Yeah, for this to feel credible you need to make sure the model doesn't figure out that you're planning to build a solution yourself.

Yes, I didn't realise how much it comes off as a critique of the author personally when I wrote it. I have added a note to that effect to the top of the article.

I think sadly all big conversations on this site are like this these days. It didn't used to be like that sadly. Z3 and some early Lean threads used to be great.

Perhaps because their concerns are different? Similar reasoning: "why invest in dependently typed languages over SMT solvers? SMT solvers are automatic, and it is way easier to add annotations to my programs"

The answer is that these technologies are not universal in trade off space.

Of course, if you can have an LLM prove something by dispatch to an SMT solver ... you want to do that (and, indeed, LLMs do sometimes do this even when working on Lean proofs)

But the space of statements that you can prove using verification with SMT is smaller than dependently typed systems.

Also, Ada/SPARK are very good and robust -- they've been around for ~50 years ... but there's been a significant amount of work in formal verification since then, right? I would be more clear that Ada/SPARK are state-of-the-art for "mission critical software" (and have been for many years), but there's been a lot of research work in formal verification of low level programming since then (Low*, for instance)

ATPs go quite a bit beyond what a SMT solver can do, however you're not stuck with just using ATPs when they are supported. You can still allow for proofs to be manually written with an ATP doesn't work, and in fact SPARK allows for this with Rocq.

Most of what I have to prove is floating-point code where a manual proof is too much of a headache to ever attempt though.

You clearly don't know shit about the whole topic, yet attack an open-source project's author who wasn't even the one posting his own project..

Why would we want the tradeoff where the LLM has to write significantly more code and where the specification needs to be more complicated? If the author is aware of the state of the art then I think they made a poor choice, but that's not the point.

Because code is trivially cheap now. LLMs churn out a shitton of code at pennies, and as technology improves their per-line cost will continue to decrease. A proof has to be written once and it's never read again. It's only important property is that it is machine-verifiable - from then on only the signature matters. Meanwhile speed of compilation matters, so an obvious tradeoff was made by the author.

my general point is about how people will vibe-code a solution without an understanding of the field, leading to worse results than if they spent a little while understanding the field and then vibe-coded their thing.

This is clearly not the case here, and even if it were, it's still a better thing than vibe-blogging clickbait shit with extra amount of Dunning–Kruger. Calling out an author who clearly works in the field for a decade or more for not knowing the topic...

Or maybe it should be a flag to indicate that there might be more to think about before handing the task of to an LLM.

Fair enough, knowing when to be and not be prescriptive about implementation details is critical too!

Humans dont let LLMs raw dog internet web searches.

That's why all your LLM requests to build something substantial should start with "run prior work research first".

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.

Yes this is precisely why experts drive LLMs so much better than novices. It’s also why I don’t dismiss pure LLM output as slop and uninteresting; even if we both are using the same LLM, I probably can’t make it output what you can make it output.

Beautifully written. Hammers for driving screws + sycophancy are horrible together.

I just tried it with chatGPT asking for whats the best hammer to drive in a nail, and it gave me a list of hammer suggestions :p . I drove it a bit further and specified wood screws and while it did point out a screw driver would be better it still kept recommending more specific hammers for driving the nails instead!

Depending on what I’m doing I’ll dedicate a few deep research sessions to building a framework. It will generate some grounding docs that go into the repo and get consumed as we go. Said docs establish terminology, widely known formulas and methods, etc.

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…

- That should nowadays be very obvious. You start any substantial work by doing research. LLMs are [perhaps surprisingly to some] good at that. They are also pretty good at doing the plumbing. That is a godsent in the hands of a good researcher and architect. And I don't have any qualms if tokens are "wasted" on research or on the precursor work. That doesn't replace reading good books on a subject but it DOES replace finding and filling knowledge gaps.

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

Pro: it can be an excellent way to learn if you realize good problems don't come easy, many such cases where I abandon something having learned from it and that's life

Con: the machine will tell you you have easily found a good problem, and engineered the perfect and necessary solution, if you let it

It's definitely AI related, though.

You just vaguely called the language "worse" without bringing a single concrete point. I can't defend my design choices without knowing what you don't like about it

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

I'm just taking it as an example

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.

You should add a strikethrough to your post and post a public apology to the author.

I don't want to change that sentence

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.

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.

He claimed the guy did no research while himself doing no research? I'm shocked! Shocked! Well, not that shocked.

To be fair, if the two words indeed don't appear in either the webpage or the codebase, it is a bit strange. It's like implementing a whole Google alternative without ever using the words "search engine".

I feel like this is the same black hole as small local models.

Things people want to be awesome and true, and things that are actually awesome and true don't intersect the way people want them to.

…so if there was an easy way to do provably correct AI code, it would be nice.

…but I’d also like a frontier that runs on my raspberry pi and a cheap fully autonomous self driving car that just uses a single cell phone camera.

Unfortunately wanting those doesn't make them exist; and people telling you they do exist usually are either a) uninformed, or b) selling something.

"horribly broken or decades behind the current state of the art"

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 "trick" is that they are not Turing-complete, they mandate termination of every expression.

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.

These stars are from version 1 of Bend

A language for LLMs will never be a compiled language. The best language for LLMs would be something that can be interacted with. Like a Lisp.

I wouldn't use SPARK either, and rather develop my own approach. The problem isn't that the proof has 400 lines of code, every modern system has large proofs (Isabelle/HOL, Lean, etc.) My latest formal proof has over 50K lines of proof. That's why AI is such a useful tool.

To be fair to Bend, I completely vibe-coded this, I just told a LLM to recreate the demo in SPARK

A vibe-coded retort to a vibe-coding tool? Ugh.

I think people don't have an intuition of LLM costs and the time saved by using it. Of course it costs but its obvious that it brings more in savings than it costs.

I'm curious, have you actually tried Bend (for more than 5 minutes)? Or are you more of an expert on this topic than the author who has been deeply immersed in this for 10 years, after it's single day of release? From an outsiders perspective it feels like this is personal to you, and you're being unfairly critical.

It will, there is just too much to do! It is a programming language. With a consistent, non-standard proof system. That compiles to GPUs. We're a small team. Please be patient

You mean the SPARK example?

Because it's a toy problem and I would definitely not take much away from it. Most proofs are basically write-only and impossible to maintain -- you are better off throwing it away. And I mean human-written formal verification here, like Coq and Agda. Take a look at formalized mathematics, they are absolutely massive code bases.

Tokens are really expensive when we have a LLM

Expensive compared to what? Vs. human writing proofs they're definitely not.

The context window becomes flooded with proof work

Context management is more art than science, but proofs are unusually good at compactation. Once proved, you can just keep the lemmas, you know,like humans do.

The problem with using subagents is that you often have to rewrite a chunk of a program in a more proof-friendly way, just saying "go prove this code, don't edit it" doesn't work. Maybe I'm underestimating how effectively subagents can communicate though and they'd be fine asking for changes.

Yes, I used Bend as an example because it is recent and high profile, and I also wanted to present my issues with it. I did not mean to conflate it with the main idea I was trying to present to the degree that I obviously did after reading my own writing as a third party would (at least to the degree that it is possible to do so).

Sorry. See the edit at the top if you haven't already.

Sorry about what? Getting caught? You entire post is based on a nasty lie about Victor and his work.

You don't have to let the ATP do everything, you can speed it up immensely with well placed assertions where it struggles. Maybe a hybrid approach is best where we run ATPs with a very low timeout to get all the easy stuff and then have a LLM write a proof using the thereoms that the ATPs were able to prove.

I was really confused when reading the article that their claim is you don't know formal verification, I was expecting something way juicer.

That is what makes Bend realistically 10x-100x faster than every alternative.

Do you have benchmarks which show this?

Hi!

I'm just leaving you a comment to counter the influx of negativity coming towards you for no reason.

I hope you are doing well and won't take all this too badly -- try to think of it as just free marketing for your project!

Have a nice day!

I was with you until this.

I use LLMs to fill code after I make all hard architectural decisions because they type faster than me, and I'd rather spend my time doing useful experiments than typing trivial functions, even though I could.

Are you being facetious? Because I've seen some bad takes from people trying to justify their AI coding practices, but this is the first one that actually made me laugh. It's clear that this public attack has you in a defensive mental state (which is perfectly understandable), so giving you the benefit of the doubt, I won't pile on and take everything you're posting too seriously.

However, I gotta point out how ridiculous this statement is, because it's the kind of thing that'd make me wonder if someone has any programming experience at all. Typing speed is not, never has been, and never will be a limiting factor in software development. "I didn't do <X> because of <reason> even though I totally could" is a pathetic cope.

It kinda reminds me of a recent post from John Carmack where he said (paraphrasing) that he originally wanted to release Idtech to the public domain as a "gift to the world", but couldn't do it because of his pesky business partners, but he totally would've done it. Let's just ignore the part of the story where he became filthy rich from licensing his software, and focus on how good it will feel to call it a "gift to the world" when an AI company integrates your code into their commercial products without licensing it from you.

Hi! I'd like to know how bend2 differs from Hoare logic or Lean?

Good point, it's similar to music and other forms of art. The qualities that the people creating it care most about often have little to do with how well it is received.

I found the post offputting because he is insinuating a few things about the author which are clearly untrue (eg, unfamiliar with the formal verification landscape) and he's using this untrue speculation as evidence of the dangers of vibe coding. Even the edit where he says swap it out with a hypothetical person who fits the description - it's still leaving in the untrue claims about the author.

It doesn't seem unreasonable to think it mean if I were to make up speculative negative assumptions about you which undermined something you've been working hard on for a long period of time.

I know nothing about the author, I'm just watching this whole spectacle unfold.

Has nothing to do with AI-hype. Anyone who is interested in Lambda calculus should find his work intriguing.

There are countless people with essentially no domain knowledge to speak of after working on the domain for a decade.

I have no idea how the original authors competency is, I know nothing about them.

There is however a strong correlation between people being influencers and kinda mediocre at what they're an influencer in - which is frankly understandable, because a large part of their skillset is usually more towards attracting an audience and making the topic interesting.

Usually the true domain experts rarely interface with the public beyond their professional capacity.

Someone can be a well-known expert in a tiny niche field, and one may be completely unaware of them, or even the whole field.

You are splitting hairs for no reason, while standing on the wrong side of this discussion.

Feel free to criticize the project on its actual content.

You have a very strange definition of expert. Most people do not have a Wikipedia page, and most experts do not have a Wikipedia page.

Muh academic ivory tower

It’s like saying Linus Torvalds isn’t an expert on the Linux kernel

It’s a poorly researched article just looking for cheapshots.

It is mean for the last point I mentioned: Taelin is very transpparent about his work which makes it easy to attack him. And what for? This post is not even a proper criticism of Bend 2, it is just trying to paint some story that Taelim is a vinecoder who does not know what he is doing, based on no evidence. If he was not transparent it would not even be known that LLMs have been used.

Because this shitty blogs' author just called someone "vibe-coding a language with no knowledge about the field" who is literally working in that very field for a decade, long predating LLMs, with numerous high-profile works.

You are on the wrong side of this whole discussion, there is only one people here who needs calling out and it's not Bend's author.

I don't know either :(

I'm not a celebrity and I don't like celebrities

No.

It would be weird to stand in line for throwing shit at someone you don't know anything about, and believing that the first guy throwing shit has an actual reason to do so.

It turns out everyone in that line is wrong..

Mudslinging isn’t appreciated, well thought out and articulated criticisms are.

The irony is that the author didn't even spend time to learn about the history of Bends author before writing this article.

I guarantee you armies of lawyers have been doing exactly what you describe for years now with existing laws, and it's only increasing.

For new legislation, you may have a point in certain situations, but even the most clueless Congress critter has people working for them who get this stuff. Whether they choose to consult them or not is, of course, another matter entirely.

This tells way more about you than Taelin. You didn't take a minute to research about Taelin, his past work, his company, and the design decisions behind the language. FFS, why people are like this.

If employer doesn't care about substantail 442 line fix, why should I?

This whole article can basically be summarized as "why is anybody building anything that already exists" gatekeeping.

Despite the fact that the entire premise is incorrect since the author of the language clearly has been shown to know about formal verification, this is basically encouraging nobody to ever post anything they work on for fear it might be "similar" to something already out there.

Is this really where we want the industry to go to all because of vibe coding?

The author of the article itself also clearly did 0 research of their own at all on the author of the language, and admits to vibe coding their own example themselves.

What the fuck are we doing.

As a resident of Bend, Oregon, checking the homepage sets off some kind of "oh look, Bend!" alarm in my brain.

Where this differs from Bend is that what we have supplied here is everything required to prove the correctness of the program, without having a LLM waste time and tokens on building up a 442 line proof from first principles. We can run GNATprove and get: `Success: all checks proved (12 checks).`

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.

The vibe coding dunning krueger damage has yet to surface, but I'm guessing it will be in the billions. I'm not even talking about the insane infrastructure investments - thousands of c suite execs are vibe coding pointless crap instead of delegating it to their team that knows what they are doing, wasting thousands on tokens if they are on enterprise API plans for zero return or spending 30$ on creating an interactive html page for stuff that should be a power point slide with a few bullet points. It's totally insane!

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

I don't know what llm you use but current llms will definitely let you know about similar things out there. So this statement is a bit incorrect.

The problem is that vibe coding makes it possible to build a substantial solution before learning enough about the problem to recognise that a much better solution exists.

We need a catchy name for this phenomenon.

It’s unfortunate because what the OP describes is a real problem. Regardless of whether or not Bend2 is realistically usable or not, the author definitely does not fit the description of the type of people who are actually causing the issue.

I fully agree with this quote, it really crystallized something i felt but couldn’t put into words.

Absolutely, and this is true to handwritten code as well. This is why code review, tests, constraints, and putting effort into the critical pieces of software is paramount to success.

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.

Self awareness means would be taking a step back and knowing if you're caught in a vicious cycle, trap, loop, pursuing something mindlessly.

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.

please, don't listen to Liam. The author is completely misrepresented in the blog-post :(

but it is not great at calling you out when you don't know what you don't know.

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

That's an excellent point and kind of summarises the tension in LLM coding between the people being told to use it (developers) and the people doing the telling (managers). The latter are laser focused on the final product, the outcome, while the former are (were) more invested in the process.

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.

Bend just serves as a useful example of my general point regarding vibe-coding as it is recent, high-profile, and has aspects that make it easy to use as an example. I don’t know anything about the author’s history with designing languages or if they actually did consider the tradeoffs below and made what I think is a poor choice

This doesn't make any sense, you're equivocating vibecoded as in "prompted by a clueless incompetent person" with vibecoded as in "implemented by an LLM". Former is used to make your point, later is used to defend the premise.

A little research before vibe-coding an entire language and compiler could have substantially improved the result because the author would have known what to ask for.

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

I am a total outsider when it comes to this topic, but it reads like the author is doing the thing they are accusing the Bend 2 guy of. Good juicy reading while I sip my coffee!

It absolutely drives me up the wall when I hear someone wrote their own language or framework because "the current ones just didn't do what I wanted to do" and then the result is a worse language/framework that the LLM and person know.

I absolutely endorse new creations when they are necessary but the people making these aren't doing it from a point of education, they are doing it purely because _they_ don't understand the framework or language that is the standard for that area.

It always always always involves a high level of AI Psychosis, that a brand new web framework is needed for your revolutionary... CRUD app?

I've been thinking about this a lot lately, because I've noticed a trend in my own life that has happened countless times: I have a tendency to look at problems that others in different fields have found difficult to solve, and think I have a great idea that could change that field. And then I push to develop my solution to that problem, run into real world problems with my solution, refine and adapt, try a different solution, run in a loop until I settle on the fact that the people who are in those fields also have great ideas, they just are more aware of the constraints and that's the reason why the hard problems don't have easy solutions.

There is an absolutely enormous amount of hubris to being an engineer. I don't necessarily think its a bad thing...a certain amount of hubris is necessary for progress to be made. Our minds are creative and we can come up with amazing things, but something in there always makes us think we can do it better than the people who are stuck doing it daily. We fool ourselves into thinking they're too stuck in their mindset to have a more creative solution.

And the funny thing about LLMs is that while they can enable our competence, they enable our hubris even more.

The problem is that vibe coding makes it possible to build a substantial solution before learning enough about the problem to recognise that a much better solution exists

As a software developer we should fear chasing "better" solutions, that path always lead to procrastination, "kitchen sink" and probably not what users wants. "Good enough" should suffice in most cases. Sure if you are building a super mega critical software to land a plane or something like that, is different. But every day software, shouldn't be treated like "carved in stone" and stuff that should last a 1000 years. Code can be cheap now (calling it "vibe coding" doesn't help).

You can create or modify something quite fast now. Better to focus on testing, documentation, making sure that software will do what is expected.

what a horrible blog-post :( Bend, HVM, Interaction Combinators, etc. isn't some vibe-coded fantasy, and the author has been working on this stuff for a loooong time.

how incredibly disrespectful :/

Feel free to replace “the author” below with “a hypothetical author who could have created the same thing”.

This is honestly sleazy, just admit you were basically way off.

All I see from this article and the whole saga is pure sadness. The situation seems unfortunate but seemingly unavoidable.

What a weird reception there’s been to bend. People discrediting the author without bothering to look him up, and then getting defensive when others point out the fact that the creator of bend has a very long very public track record of work in the field.

The irony of this post talking about vibe coding and not doing one’s research, on only not have done even the slightest inkling of research themselves (heck, even asking an LLM about the author would for sure have turned something up).

I hope people will give it a second look, and not just stop at this post which is a gross misrepresentation of Victor Taelin’s work.