Thread

Bend – a language that blocks AI mistakes via proof and runs on GPUs

616 points · 327 comments · nicolas-siplis

stschaef · 1789680077 · focus · HN ↗
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 <a href="https://github.com/um-catlab/cubical-categorical-logic" rel="nofollow">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 <a href="https://arxiv.org/abs/2401.15258" rel="nofollow">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
1. killerstorm · 1789682922 · focus · HN ↗
  Victor Taelin has been doing interesting PLT research for 10+ years.
  I suggest you read his history: <a href="https://gist.github.com/VictorTaelin/77fd5a2a8a4a07e1da6157ebca3c7cf1" rel="nofollow">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": <a href="https://github.com/HigherOrderCO/HVM1" rel="nofollow">https://github.com/HigherOrderCO/HVM1
  1. stschaef · 1789683628 · focus · HN ↗
    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
    killerstorm · 1789686262 · focus · HN ↗
    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 : <a href="https://github.com/VictorTaelin/Interaction-Type-Theory" rel="nofollow">https://github.com/VictorTaelin/Interaction-Type-Theory that's 3 year old, pre-dates Fable, but OMG doesn't look like a paper.
    stschaef · 1789687470 · focus · HN ↗
    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
    killerstorm · 1789689550 · focus · HN ↗
    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: <a href="https://bend-lang.com/bender" rel="nofollow">https://bend-lang.com/bender

Open on Hacker News to reply ↗

Unofficial Hacker News client; not affiliated with Y Combinator.