stschaef

I am relatively new to the site, and I guess I’m just surprised by this. I thought the dweebs here would mostly care about the technical content

But I guess I totally ignored the YC context in that interpretation

I’ve posted a follow up somewhere else in this thread about how I can retroactively see why some people would read rudeness in my comment. Even though this isn’t intended, I agree I need better choice of words

What I didn’t understand when expressing confusion with the responses, and still don’t, is the personal nature of the response. It wasn’t pushing back against anything I said really, moreso it tried to bring up the credentials of the speaker; and, I guess this feels a nonsequitr

Like, if I say “I have these problems with thing X”, it doesn’t really matter who made X. Sure, it’s context I didn’t have and there is something to be gained in saying it; but, it doesn’t really change any of the critiques I had. Appealing to the authority of the creator doesn’t engage with nearly everything I said

Yeah, reading it again it sounds far bitchier than initially intended. Thanks for the response

I was writing the comment very stream of consciousness and not really think about how it may come across

If I were trying to boil down what I’m attempting to communicate, it would be 1. The project seems cool, but it’s also making some very strong claims that I’m hesitant to accept

2. The coolness of the thing is undermined by the presentation of it. It comes across as putting the cart is put before the horse, and the overly strong claims and marketing speak read as trying to rhetorically sway the audience rather than engage with them technically.

3. I genuinely am happy that the creator made this, but modulo the above worries I think it should be reeled in a bit. In part because of the concerns I have about the content, and further because it is the kind of language that I expect others to have a strong averse reaction to. Possibly to the point of also reaching the top of HN with their negative response

To a friend, it might be easy to capture some of this message with “you sounds sus af”, but to a stranger in the internet I see how I just sound like a jerk. Words do matter, and I think I’ll be more careful about this in the future

I posted a sharp critique in the original discussion, aiming to be civil while critiquing the project. I may have been a bit terse, and would probably rephrase some of it now to avoid confusion, but I don't think I was ever outwardly disrespectful.

I received several very emotionally charged responses centered in the personal credentials of the author. They felt very out of place and did not engage substantively with any of the things I said. It was indeed very weird

The author, who I hadn't heard of before yesterday, actually seems like a cool dude. He was quite responsive, normal, and engaged with my feedback, which makes other random accounts being offended on his behalf all the more uncanny

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?

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

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

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

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

This reads very vibecoded, but putting that aside...

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

Do you have any evidence that neoemacs witnesses any speedup? It's a neat idea but I don't quite get why I'd want this without seeing some evidence

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

I immediately received the following error :|

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

I don't see what we gain for the mention of category theory here, and I find the categorical content in the book to be pretty buried.

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).