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

Hey, I get a 404 from that link.