Yes, there's a lot of vibe-coding in many places, but the critical parts (compiler, runtime, kernel) are human designed, and the kernel has been extensively audited by human. All of it is my own design and architecture, and I'm a human, I think. We'll prune AI slop over time. The project is big, and we're a small team.

1. The paper explains it well (sadly it is written by Claude for now, but it is accurate):

https://github.com/bendlang/bend/blob/main/paper/BendRT.pdf

In short, we implemented a complete allocator, garbage-collector, closure evaluator and functional evaluator, on the GPU (with zero interaction net overhead this time). We then use a very simple (for now) scheduler that spreads binary recursive calls as to saturate all CPU or GPU cores, depending on where it is running. This is the simplest thing that works fast. In the future, we want to have a more flexible task stealing queue, but contention destroys GPU performance, so, that's the best thing that works, for now.

2. Benchmarks aside, large scale verified programs would run much faster on Bend for a simple reason: Bend is fully explicit. It has no tactics, and it does zero compile-time search. As always: the less a computer does, the faster it runs. This is a tradeoff. In exchange, Bend code is substantially more verbose than Lean, and it is more laborious to write Bend proofs. I argue this is the right tradeoff, because AI write proofs, and AI time is cheap, while bugs take human time, which is expensive.

3. Sorry I'm not proud of the commit history

4. I don't think it is worthy publication because the core idea is simple. We just use QTT-like linear types to fully prohibit runtime closures. So, paradoxes like Russel's and Girard's are blocked. In exchange, functions like List.map are not expressive (without templates). So it is not a research breakthrough. I just made a conscious trade here, which makes Bend way closer to C or Rust, than to Haskell or Lean.

5. Will patch.

Great questions actually, and surprisingly respectful. I appreciate it a lot.

1. thanks, I'll try to take a look later at this. Most of my skepticism was rooted in a personal-hell I endured when trying to parallelize SAT-solving with GPUs...which didn't go well because its hard to share across workers effectively. Another thing to note, I'd frown upon using Claude-written works for communication between humans. If the ideas are yours then it should be feasible to write the paper. Many people will take "Claude wrote this paper" as a big sign telling them to ignore it

2. With no offense, but until it is demonstrated that this is useful for larger verified software projects I will be intensely skeptical; and, I'd advise not making claims like this until you have empirical evidence

4. Assuming this all holds air and isn't AI-bs (I'll make no claims in either direction), then yeah I'd say its valid research. To be clear with what you're claiming here, you're giving the impression that you have a GPU-accelerated proof assistant that is 2 orders of magnitude faster than Lean. If true, then that's a big and interesting contribution

Best of luck with everything. I certainly understand the frustration with how slow proof assistants can be, and I hope that we as a community can significantly speed them up

2 isn't a big claim though, I think anyone developing Lean or Agda would agree these would be much faster with zero inference, unification or search? They'd just complain the language would become unergonomic, and that's true. Bend is very verbose.

Thanks and your feedbacks are reasonable, I appreciate

After looking through things a little more, I think I may have had some misunderstandings. Would you be willing to answer a few more questions? I will also take a closer look at the papers at some point, so apologies if these are redundant

1. When I see a comparison of a new proof checker to something like Agda/Lean, I initially evaluate them as systems for formalized mathematics, but I don't think you're making claims of that nature. Would you say that you'd expect, say, the new giganto proof of Fermat's Last Theorem to be expressible in Bend and faster than the corresponding Lean proof?

2. If the answer to the last one is no, that's not expressible, then what is the class of propositions/types that you express? My initial reading was that it was the whole of affine dependent type theory

3. Is the GPU used at both runtime and compile time?

1. I do, but probably not in the current version, since I believe these proofs probably need full closure cloning to be ergonomic.

2. You can express anything actually, because you can clone data, just not functions. So, anything you could implement with datatypes (i.e., without cloned closures), you could probably also prove. But again, people use and abuse closure cloning a lot in Lean. So, how ergonomic would that be? I don't know. It is less about expressivity and more about ergonomics.

3. No, just in the runtime for now. Checking proofs on the GPU will happen when we implement Bend in itself.

Hey, I get a 404 from that link.

fixed ty

Funny seeing you here--I'm in 590 with Max and Eric. I saw Agda and guessed it was someone from the group :)

Victor Taelin has been doing interesting PLT research for 10+ years.

I suggest you read his history: https://gist.github.com/VictorTaelin/77fd5a2a8a4a07e1da6157e...

before making slop accusations. Older variant of what became Bend is 5 years old, so definitely not "vibe coded": https://github.com/HigherOrderCO/HVM1

This is a very strange comment

First, I think everything I said was respectful and rooted in the content of the Bend page rather than an assault of Victor as a person. I’m very confused by your random appeal to the author’s reputation here. He seems like a smart and cool dude, and I still have things to say in response to what’s presented here for Bend

Second, the paper is openly written by Fable 5.1, so I’m not making any unfounded accusations

Victor put 5+ years of research into this. You can find many of previous versions (which use different approach, do a different kind of a thing, etc.) on the github. "Bend2" in particular have been in development for 2 years.

Calling this "a random vibecoded project" is rather disrespectful, don't you think?

Regarding the paper, he states it clearly "designed by the human author". That's not at all the same as just asking Fable to write a paper. I mean the important thing is ideas, not the way they are described.

Please tell me how "I'm glad you're having fun vibecoding" is not disrespectful?

I thought that you thought Bend web site is all that is to it and wanted to point to relevant information. But if you think that "having fun vibecoding" is an appropriate thing to say to somebody who spent many years doing research, I don't know what else to say.

Again, as a "proof of research" take a look at : https://github.com/VictorTaelin/Interaction-Type-Theory that's 3 year old, pre-dates Fable, but OMG doesn't look like a paper.

Again, very strange

External parties can’t do any meaningful discrimination between human and agent effort when the agent is doing the communicating. One may only read what’s there

I’m not saying that the author is inept or that they have done no work. There can be plenty of great underlying mathematics behind something that is vibecoded.

The reason I worry about the use of agents here is not because it invalidates any ideas or research done by the author; rather, it editorializes and oversells. It presents the claims of the work as an all encompassing solution to all of the worlds problems

There may very well be tons of great ideas here. However as presented, it reads as though the language is the solution to creating vibecoded apps and is equipowerful to state of the art proof assistants while being orders of magnitude more performant. That is a huge claim that has not yet been substantiated, and I do not believe that solely a human is currently making that claim

That's a start-up style marketing: when you make a product you focus on a big vision and positive sides and de-emphasize weaknesses. I'm afraid that's actually 100% Victor's decision to do it this way, and it seems to be working in terms of generating hype: it got ~4k likes on X, which is a lot for a new language.

Regarding substantiation -- they released source code and demos. As far as I understand, the weakness is that proofs are very verbose as there are no strategies. etc. However, they are making a separate service for making these proofs using proprietary technology: https://bend-lang.com/bender

> Again, as a "proof of research" take a look at : https://github.com/VictorTaelin/Interaction-Type-Theory that's 3 year old, pre-dates Fable, but OMG doesn't look like a paper.

Yes, it doesn't look like a paper at all. I can see the idea, and it's an interesting idea, but no proofs that it works, no measurements, and no proper citations.

Nobody claims Victor hasn't done a lot of research. But academically inclined people typically expect claims to be substantiated either formally or empirically or both.

A complete implementation have been released, how is that not a substantiation?

Academic people might have more trust in a paper which when through a lengthy publication process. But if you think about it, it's not a better proof than a direct access to the thing. It used to be hard to try out software but with modern tech it literally takes minutes...

How do you know the implementation is complete or that it works well?

Have you evaluated it?

Wouldn’t you be inclined to withhold any claims of anything being substantiated until it’s actually been evaluated?

Wait what? Have you? Why are you posting passive aggressive unfounded dismissals posing as questions?

No, I have not, so I don’t post baseless dismissals. I don’t call authors sus af and I don’t call people’s work vibe coded slop.

Have I?

Are you arguing with me or the parent who actually called it “sus af”?

To pick on a few examples:

> a random vibecoded project

> If this weren't slop...

> I'm glad you're having fun vibecoding, and I like that you're interested in this area of research/engineering

These impute both his motives ("fun") and particularly his level of seriousness ("random project" and "I like that you're interested"—imputing passivity, as opposed to "are studying" or "are researching," which would be more appropriate given the amount of time invested). They're all dismissive and patronizing.

I would actually regard this as bullying. Some feedback.

(I suspect you're an academic, either a researcher or student. I know from my own experience that bullying is endemic in many academic research environments, so if you find the negativity you're receiving "strange," I suggest finding a therapist, who may help you understand how your communication habits could be negatively affecting other people and unintentionally damaging your relationships.)

stschaef‘S comment was on topic and a critique (albeit sharp) of the work.

Your comment is a personal attack though, and much closer to bullying.

FWIW the author can and has spoken for themselves and noted the comment was “reasonable”.

In my culture it was ad personam, not even trying, and it’s fantastic that it’s been pointed out in a respectful way and reacted to with calm by all participants.

The author was very polite to even reply at all.

> Your comment is a personal attack

I don't think stschaef is a bully; in fact, if my guess that he's a researcher is correct, I think he's likely highly altruistic (I've never met him, but categorically, researchers are people who chose a difficult, low-paying job doing work of great societal value).

However (again if my guess is right), I think he could easily be in an environment where narratives about people's work being worthless, about them being stupid or unserious or otherwise beneath consideration, are common. It's a reaction to the fact that in any field, the amount of research produced is overwhelmingly more than anyone can digest. There's a lot of unstated anxiety and guilt about that, on the side of both writers (who worry no one will read their research) and readers (who feel obligated to try to read everything and are eventually, inevitably overwhelmed), which IMO is itself a product of the basically altruistic nature of most researchers.

The overwhelming reality of being a researcher is an inescapable, empirical fact, but the narratives people create around that reality, about peoples' work and its worth, are not. People are hard-wired to be sensitive to rejection, because humans are a cooperative species and social acceptance is existential to each of us, and the problem is that a lot of researchers, who are steeped in these narratives, are trapped in a self-reinforcing cycle of community attachment threat: their research sucks (or could start to suck if they ever went on vacation), and the research of most of the people who are evaluating them sucks too.

What if these stories about the worth of people and their work aren't true? Guess what: one can do amazing research and it still goes nowhere, because ultimately it's not possible to control other peoples' behavior. If one's goal in research is acceptance and respect from the community, they should consider that they're gambling their time, energy and youth on an outcome they can't control. The research community can be a fine place, but it's not special—one does not have to be a researcher, and if the experience of being a researcher sucks for them, they should quit, because living a good life is their responsibility.

I grew up around this attitude, and children are particularly sensitive to attachment threat. It's bad enough that researchers tell these stories about each other, but once these narratives and communication patterns about peoples' work and its worth leak outside the context of the research community, they run right into the reality of human attachment and the expectations of communities that aren't the research community. I'll say about my own family: I think they were good people who learned an unhealthy, judgmental attitude (towards themselves as well as others). I think they immiserated themselves (and inevitably the people around them), because perpetual attachment threat had traumatized them into false sense of obligation, and I wish they had quit.

Even if one stays, they should understand the mismatch between the narratives and culture of the research community, and they needs and expectations of most people outside of it. That was the context of my comment. I think it's fine if stschaef doesn't like TFA and doesn't find Bend novel or interesting, but my analysis of the sentences quoted reflected my organic reaction to them, and I stand behind it and my other feedback.

Commit history is back!

You expect an arxiv only paper to be cited? Do you even know fuck all about scientific research? Do you think someone can slap "Foundations of" in an arxiv title and we are mandated to cite it?

Yes, I'd expect a 2 year old preprint from a rising research in this utlra-niche field to likely be discussed when someone is claiming to have a sweeping solution on exactly the same research question

Maybe not necessarily so, but while looking through the paper's bibliography I get the sense that these were AI-gathered references because there seems to be gaps in the current literature on this topic