Bend – a language that blocks AI mistakes via proof and runs on GPUs
Thread
Unofficial Hacker News client; not affiliated with Y Combinator.
Bend – a language that blocks AI mistakes via proof and runs on GPUs
Unofficial Hacker News client; not affiliated with Y Combinator.
stschaef · · focus · HN ↗
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
killerstorm · · focus · HN ↗
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
stschaef · · focus · HN ↗
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
msteffen · · focus · HN ↗
> a random vibecoded project
> If this weren't slop...
> I'm glad you're having fun vibecoding, and I like that you're interested in this area of research/engineering
These impute both his motives ("fun") and particularly his level of seriousness ("random project" and "I like that you're interested"—imputing passivity, as opposed to "are studying" or "are researching," which would be more appropriate given the amount of time invested). They're all dismissive and patronizing.
I would actually regard this as bullying. Some feedback.
(I suspect you're an academic, either a researcher or student. I know from my own experience that bullying is endemic in many academic research environments, so if you find the negativity you're receiving "strange," I suggest finding a therapist, who may help you understand how your communication habits could be negatively affecting other people and unintentionally damaging your relationships.)
ModernMech · · focus · HN ↗
Your comment is a personal attack though, and much closer to bullying.
FWIW the author can and has spoken for themselves and noted the comment was “reasonable”.
msteffen · · focus · HN ↗
I don't think stschaef is a bully; in fact, if my guess that he's a researcher is correct, I think he's likely highly altruistic (I've never met him, but categorically, researchers are people who chose a difficult, low-paying job doing work of great societal value).
However (again if my guess is right), I think he could easily be in an environment where narratives about people's work being worthless, about them being stupid or unserious or otherwise beneath consideration, are common. It's a reaction to the fact that in any field, the amount of research produced is overwhelmingly more than anyone can digest. There's a lot of unstated anxiety and guilt about that, on the side of both writers (who worry no one will read their research) and readers (who feel obligated to try to read everything and are eventually, inevitably overwhelmed), which IMO is itself a product of the basically altruistic nature of most researchers.
The overwhelming reality of being a researcher is an inescapable, empirical fact, but the narratives people create around that reality, about peoples' work and its worth, are not. People are hard-wired to be sensitive to rejection, because humans are a cooperative species and social acceptance is existential to each of us, and the problem is that a lot of researchers, who are steeped in these narratives, are trapped in a self-reinforcing cycle of community attachment threat: their research sucks (or could start to suck if they ever went on vacation), and the research of most of the people who are evaluating them sucks too.
What if these stories about the worth of people and their work aren't true? Guess what: one can do amazing research and it still goes nowhere, because ultimately it's not possible to control other peoples' behavior. If one's goal in research is acceptance and respect from the community, they should consider that they're gambling their time, energy and youth on an outcome they can't control. The research community can be a fine place, but it's not special—one does not have to be a researcher, and if the experience of being a researcher sucks for them, they should quit, because living a good life is their responsibility.
I grew up around this attitude, and children are particularly sensitive to attachment threat. It's bad enough that researchers tell these stories about each other, but once these narratives and communication patterns about peoples' work and its worth leak outside the context of the research community, they run right into the reality of human attachment and the expectations of communities that aren't the research community. I'll say about my own family: I think they were good people who learned an unhealthy, judgmental attitude (towards themselves as well as others). I think they immiserated themselves (and inevitably the people around them), because perpetual attachment threat had traumatized them into false sense of obligation, and I wish they had quit.
Even if one stays, they should understand the mismatch between the narratives and culture of the research community, and they needs and expectations of most people outside of it. That was the context of my comment. I think it's fine if stschaef doesn't like TFA and doesn't find Bend novel or interesting, but my analysis of the sentences quoted reflected my organic reaction to them, and I stand behind it and my other feedback.
[deleted] · · focus · HN ↗
[deleted]