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.
    etiamz · 1789690257 · focus · HN ↗
    > 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.
    Yes, it doesn't look like a paper at all. I can see the idea, and it's an interesting idea, but no proofs that it works, no measurements, and no proper citations.
    Nobody claims Victor hasn't done a lot of research. But academically inclined people typically expect claims to be substantiated either formally or empirically or both.
    killerstorm · 1789692958 · focus · HN ↗
    A complete implementation have been released, how is that not a substantiation?
    Academic people might have more trust in a paper which when through a lengthy publication process. But if you think about it, it's not a better proof than a direct access to the thing. It used to be hard to try out software but with modern tech it literally takes minutes...
    steego · 1789707011 · focus · HN ↗
    How do you know the implementation is complete or that it works well?
    Have you evaluated it?
    Wouldn’t you be inclined to withhold any claims of anything being substantiated until it’s actually been evaluated?
    baq · 1789708663 · focus · HN ↗
    Wait what? Have you? Why are you posting passive aggressive unfounded dismissals posing as questions?
    steego · 1789735909 · focus · HN ↗
    I’m not being “passive aggressive” with an “unfounded dismissal posing as a question”
    The person I am responding to made a SPECIFIC claim when they said, “A complete implementation have been released”
    They then ASKED, “how is that not a substantiation?”
    Uploading code does NOT substantiate anything.
    The code must been executed, tested, analyzed and/or verified in order to substantiate ANYTHING.
    We are in limbo because MOST people are JUST seeing the code now. Almost nobody has evaluated it.
    BTW, I got the Discord announcement BEFORE I saw the HN announcement (Because I’m not a hater or a bully) and I started looking at the Lean code as well as the TypeScript compiler.
    Have YOU been evaluating it? Do you actually have an informed opinion, or are you here to fight the bullies?
    baq · 1789760305 · focus · HN ↗
    No, I have not, so I don’t post baseless dismissals. I don’t call authors sus af and I don’t call people’s work vibe coded slop.
    steego · 1789763275 · focus · HN ↗
    Have I?
    Are you arguing with me or the parent who actually called it “sus af”?

Open on Hacker News to reply ↗

Unofficial Hacker News client; not affiliated with Y Combinator.