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
(author here) Bend1 indeed has no significant active userbase
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
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.
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.
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 cannot understand the hostility being directed towards you for this project. It seems very interesting. Your reply was very well thought out. I am very confused.
Seems to be a fair deal of astroturfing going on for some unknown reason. I can't tell if it's intentional to drum up controversy, or it's genuine because people are bitter about this for some reason.
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.
Note that using linked lists for strings is actually more "parallel friendly" because you can take the head/tail and spread it around 16k GPU cores in O(1), unlike in Haskell, unlike arrays, which require a linear copy, becoming quadratic. So, the right "default type" isn't that clear on Bend, because GPUs behave very differently from CPUs.
That said, yes, we definitely should have a compact Text type. I'll add it over the weekend.
Though also, parallel processing strings and other non-numeric data on that level of granularity is, IME, typically less performant. The parallelism rarely manages to offset the performance penalties incurred by decomposing the problem in a parallel-friendly way. Even on a single machine you’ve got to think about whether organizing the data in a parallel-friendly way also makes it less cache-friendly. For example, a linked list of Unicode code points is 12 bytes per character, and each character might be on a completely different cache line. Depending on language a UTF8 buffer might be 1/10 the size and have a much more compact layout in memory.
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.
I dropped out of Federal University of Rio de Janeiro to study this subject independently, because I was passionate about it, and I spent nearly 10 years doing so, daily, on weekends. That's what I do.
Bend proofs being verbose has nothing to do with me not knowing that inference, unification, or program search exists. Kind had these, 5 years ago. In fact, I've also been researching the later, and I built SupGen, which overperforms every published symbolic program synthesizer in the literature by 10x or so. This is unpublished yet, but you can find my posts about it 2 years ago on X (I'm @VictorTaelin).
So, why is Bend verbose???
Because it makes it fast. It is intentional. It is my vision that a good proof language should be fully explicit, because this reduces proof-checking time significantly. That is what makes Bend realistically 10x-100x faster than every alternative.
But wouldn't that mean it is much harder to write it?
No. As you said it yourself, we have tools that can fill these proofs today! Not just AI models. You can apply these tools to produce Bend proofs, while the language itself remains a thin, dumb proof kernel that does one thing, and does it well.
If nobody is reading these proofs (because they're written by AI and automated tools), then, it is, in my opinion, irrelevant, as proofs will eventually become a layer nobody looks at, just like generated assembly.
Of course, I could be wrong here!
But it is misleading, if not just a bit malicious, to claim I "vibe-coded" a language without knowing about a field I've spent a decade researching about.
Every single part of Bend is an intentional choice I made after considering every alternative. 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.
Incidentally, deciding what I should NOT include took me way more time and effort than any line that was shipped, and there are perhaps millions of lines of code, manually written by me, that I threw away, backing up these 4k that went into the final design. An artist once told me you must first paint a Rembrandt before you can draw a cartoon that's simple in the right way, yet that might mislead someone who has never drawn into thinking you don't know what you're doing. I guess.
> But it is misleading, if not just a bit malicious, to claim I "vibe-coded" a language without knowing about a field I've spent a decade researching about.
Sorry. See the edit at the top if you haven't already. I didn't realise how much it came off as a critique of you rather than a particular approach to software engineering.
It's easy to write something and have a model of what you're writing in your head that is massively different from how someone else will read it without realising, not that that excuses it.
---
I disagree with LLMs manually writing proofs without other tools doing all the work they possibly can ever being a good solution for a couple of reasons:
1. Tokens are really expensive when we have a LLM spending hours hacking aware at a proof, not to mention generating those tokens is slow.
2. The context window becomes flooded with proof work rather than work on the original problem, which will lead to a worse solution. LLMs are demonstrably worse at writing code when you continue a session on a new task instead of starting a new one.
> It is my vision that a good proof language should be fully explicit, because this reduces proof-checking time significantly.
We can cache the results and help the checker along with assertions rather than throwing out all the smart parts of the checker.
I would encourage you to think more deeply about the assertions you're making here.
I've done a fair amount of work in this space as well, specifically my main toolbox of formal verification tools in the past have been Rocq, Idris, Dafny, and TLA+, and I can say that I've come away with roughly the same set of tradeoffs as what LightMachine describes in his comment.
Current formal verification tools are often very slow precisely because they try to reduce the number of lines of code that are required to write a proof. By making proofs more verbose and more explicit, proofchecking is sped up immensely (my own experiments check out with what LightMachine is saying here; indeed I've seen even greater speedups in the range of 100-1000x).
It makes far more sense to pay a series of one-time costs in LLM tokens that reduces your compilation time from 1 hour to 1 second than to pay the 1 hour compilation cost again and again (these are not exaggerated numbers for larger projects). This is especially true because with modern LLMs, it's usually just fire and forget and let it churn in the background than anything else.
Caching and incremental compilation has a lot of limitations, e.g. for CI. This is the promise that languages like GHC Haskell have promised for a while that always gets blown away by the other side like OCaml where global compilation is just so fast that you don't have to deal with those limitations.
1. LLM inference is cheap compared to the cost of a bug, and you can use tools to automate the proof-work, as you said so yourself.
2. Why would it? The AI shouldn't load already completed proofs, only their type signatures (which are one liners). Sounds like you're projecting bad context management?
Caching only works until you change a deeply nested constant. Then you must wait 2 hours as Lean re-checks every transitive dependency of a massive simp-ridden codebase. Also, first time check time IS relevant to UI. Nobody wants to wait 2h to start using a library after they first download it. Perhaps you don't mind that but I do; that's the kind of bad UX that made me go for that design choice on Bend. Which again, may be wrong or may be right. But it was intentional.
Having a checker that is just fast by construction, regardless of caching, was a top design priority, and I weighted it over verbosity in a layer I believe nobody will be reading anyway.
> you can use tools to automate the proof-work, as you said so yourself.
The language doesn't appear to be designed around supporting existing tools (either by exporting to Why3 or manually interfacing with existing tools). I'm not against shipping the whole proof or storing it on a cache server, I'm against the idea of having a LLM write it all. Even having the LLM only write proofs for subprograms that take a long time for ATPs to prove would work.
For the example in the article, the LLM had to write it exactly once without any iteration and it proved in a second, which I assume was mostly startup time. Having a LLM write 442 lines instead, which I assume also needed some iteration, is a tough sell in comparison.
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
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.
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.
Just don't use frontier models by American labs. Chinese models are much cheaper and competent enough for most stuff
> 2. The context window becomes flooded with proof work rather than work on the original problem,
This can be solved by doing proofs in subagents. You can even have a tree of agents, for demanding proofs. They can share a database or otherwise have communication channels if some of them stumble upon something relevant for another agent
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.
Post author just wanted quick clicks based on kneejerk heuristics based attacks on Bend. Now he’s doing gymnastics all over this thread to mitigate what he said. Sad and disappointing.
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).
> 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.
The project got a lot of attention at launch, but it wasn't really ready to be used back then. There were too many limitations, like u24 numbers (yes), 2 GB memory limit, pervasive strictness (if-then-else executed both branches). It was just not practical.I think (hope) that explains a lot of it. But honestly there is also my own failure into making the language actually be used, rather than just a viral moment :( I hope it will be different this time!
reply