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?

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

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

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

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

1. How does this benefit from GPU parallelism? I don't know much about implementing proof assistant, as I am just a user, but its my understanding that these tasks aren't amenable to running on a GPU.

2. The comparison to Lean/Agda/Isabelle/etc have no meaning without understanding what programs are being used for comparison. I also so far have no reason to believe large-scale verified programs would ever adapt to Bend. For instance, I have a large software verification project written in Cubical Agda https://github.com/um-catlab/cubical-categorical-logic it's not clear to me how one would even begin to port this over to Bend, especially given the dependence on cubical

3. Single commit history is hella sus

4. Bend uses "an affine dependent type theory". Substructural dependent type systems are an active area of research. If this weren't slop, I'd expect such a system to be worthy of publication at a top programming languages conference. It sounds quite unlikely that a random vibecoded project with a Fable-written paper has worked out all of the kinks

5. I would've at least expected this paper to be cited https://arxiv.org/abs/2401.15258 but it is noticeably absent

I'm glad you're having fun vibecoding, and I like that you're interested in this area of research/engineering, but you are wildly overstating what you have here and sound sus af

I've also considered the possibility of a Rust rewrite of emacs, but after doing some more digging it seems like it may not be worth the effort. The remacs project seems to have been abandoned. I think they hit diminishing returns

Moreover, this ready like AI slop

This is pdfTeX, Version 3.14159265-2.6-1.40.21 (SwiftLaTeX PDFTeX 0.3.0) (preloaded format=swiftlatexpdftex) I can't find the format file `swiftlatexpdftex.fmt'!

Likewise for XeTeX

If we're talking about categories, then we should be able to provide definitions of objects and morphisms clearly and independently. I guess I expected this to give denotational semantics of machine learning in an appropriately structured category, and then afterwards we can provide an implementation of these abstractions in Rust; however, this doesn't seem to be the case in this book. Rather, the category theory does seem somewhat stapled on. I wished that this would talk about things like Markov categories (or some other appropriate appropriate semantic domain) and then characterized machine learning algorithms via adjunctions between certain categories, such as in https://link.springer.com/article/10.1007/s44163-025-00707-w

As it's written, I don't see much of an opportunity for deriving theorems about the implementation from abstract nonsense, which, to me, would be the biggest strength of such a categorical description. This seems to be a simultaneous high-level introduction to Rust, machine learning, and category theory. The writing suffers from this, as the reader doesn't have much of an opportunity here to detangle these ideas from each other or see how one aids in understanding the others. Instead, they are all provide at once, and to an insufficient level of detail (for the amount of skimming that I did).