alt Hacker NewsYes, 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.
Replies
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. 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