Claiming super fast compile times with super fast runtimes faster than LLVM and the compiler is a single typescript file 6k characters long of AI slop. Jesus.
Glad to see a new release of Bend, fascinating cutting-edge stuff.
I had to look up "gambiarra": a Brazilian expression that means to use improvised methods to solve a problem with any avaiable material.
Totally understandable, I think you did the right thing by releasing early, even if it's still in rough shape, to get some public feedback. This forum can be a hit-or-miss, sometimes even great projects are not appreciated (and the opposite too). But I imagine some people are in the target audience who will see the project and actually explore the language, and follow along with its development.
Victor Taelin's work (HVM) got me interested in interaction combinators as a compilation target. I'm now working on an implementation as part of my Uni research. Cool to see Bend 2.0 release!
Then you might be interested in Marc Thatcher's recent PhD thesis dedicated to interaction nets [1]. A great exposition of interaction nets through multiplicative linear logic's proof nets, and several novel contributions like productivity analysis for interaction nets.
...did they just squash the repo to 1 commit for v2.0.4? Why? Yall should know that in this age of AI trust is the real currency... and nuking your history is one hell of a way to raise eyebrows.
> Enjoy bug-free, fast vibe-coded apps! Hints: ask it to write laws for whatever should never break, and to parallelize everything you want running fast. Bend is
young: if anything goes wrong, ask it to open an issue.
Emphasis mine. I don't want to be snarky but like... come on.
Erm, because it looks weird? Do you know any other language projects that squash their repos down to 1 commit? That's a destruction of trust, which is kinda important if you want people to build on your language.
Virtually everyone has AI slop in the commit history. No one's judging you for the commit history. Everyone's code smells, but the fact that you're ashamed/hiding it is... odd.
I for one don't find it strange at all that he squashed the commit history. I suspect many feel similarly. You've demonstrated that you're quite taken aback by it, but without explaining anything wrong with it. It is not a "destruction of trust".
I mean... If you wanna build your project on a language that has no auditable history, reproducible builds, artifacts/releases, force pushes and breaks literally EVERY fork/PR, has no way to build or even see v2.0.3, and doesn't have changelogs... then I guess that's cool. You must be a trusting person; I unfortunately am not like that.
To give you a concrete reason why you should care to preserve the exact history and why it’s a matter of trust, you report the pinned SHA head of the benchmarks you ran in your paper. When you destroy the history you make it hard for people to duplicate your benchmark results. Why report the SHA if you are going to destroy the history?
There is just a lot of private data and even proprietary code (like SupGen) in the commit story, so I just squashed it. I didn't think that'd be an issue? Why?
Jokes aside, I think the idea is that the law is simple to code, the proof that it holds is where the agent is responsible. This probably becomes less true though as you try to express more complicated laws.
Heh, it's like we all need to collectively read I, Robot yet again, and the myriad of SF books on the subjects. Black and white quickly dithers to grey.
The point of those books is that robots can be perfectly rational, and for a useful robot we would expect them to be.
What they aren't is moral, because of the orthogonality principle: you can't use facts and logic to discover correct moral beliefs. Morality is about values, goals, and the definition of "good". They must be provided to the robot by its creator, and those are things that are very hard to precisely describe in a way that is fully consistent with the speaker's intent in all possible scenarios, and agreeable by all other people.
writing specs is hard. For instance the easiest way to comply with "player should never reach the flag" is to disable movement completely, so then you have to specify "player should never reach the flag while still being allowed to move" and so on (liveness). It's not practical for most programs
Yeah, in small examples it's pretty neat: Define a "sorted" property, write a law that checks that the list is sorted and contains the same elements and someone else implements the sort and together with a proof for correctness. However larger software systems have an exponentially larger surface for reasonable and unreasonable edge cases. When I hit ctrl+s in my editor I expect that my cursor does not change colour, that the window does not minimize, that the program does not crash if there is no disk space left and so on. I don't see how this does not devolve into "negative space programming" where the user would have to anticipate and constrain every possible unwanted behavior of his software.
>> When I hit ctrl+s in my editor I expect that my cursor does not change colour, that the window does not minimize, that the program does not crash if there is no disk space left and so on.
HN staff: someone posted before me. Could we change the title to
"Bend - a language that blocks AI mistakes via proof and runs on GPUs"?
Everyone: feel free to ask any question, but I'd be highly appreciative if you could be a bit civilized and respectful this time. I've worked on this for 1 year, nearly 16h/day, 7 days a week, and I'm giving it for free. You need not to use it. So, I'd be thankful if you could point occasional failures politely rather than throwing me in a lava pit.
I'm confused - could you explain how the board/flag animation relates to Bend's compile time checking? Is it actually a direct demonstration of Bend running a check?
Could you recommed literature (preferrably a single book) that does not require prior knowledge and allows to fully understand the logical foundation of it?
(Why it is done the way it is, what problems are solved by affinity, why closure can be called at most once, how a function that never returns can prove anything, and everything else)
There isn't a single book that covers all of it... Bend's theory touches various domains (dependent types, substructural types, termination). And then there's the runtime, compiler, GPU kernels...
If you mean about the type theory specifically, "Type Theory and Formal Proof by Nederpelt and Geuvers" is a good introduction. Not sure what I'd recommend on linear types, no book I know of is very introductory? Perhaps "Idris 2: Quantitative Type Theory in Practice", which is a language with similar foundations to Bend, and the author wrote a book on it (and inspired myself!)
I like the idea of a language intended from the start to be proved and it seems very compelling given coding agents. It's a good idea that others don't see coming -- so expect it to be frequently misunderstood and even verbally abused!
Amazing work, one question regarding the guide, it states:
> That same file is the CPU program and the GPU kernel: clang builds it for the host, Metal or CUDA builds it for the device, so a `!` runs the exact same code on either chip.
What exactly is this saying? The guide doesn't really explicitly define `!`, and it's unclear from this sentence whether it's saying that, "clang builds it for the host and Metal, and CUDA builds it for the device", or if it's saying, "clang builds it for the host, Metal, and CUDA, and builds it for the device", or something else entirely.
It just means that Bend compiles to a single .c file, and that file compiles to either Metal or CUDA, via macros, depending on your target. This shouldn't be relevant to most users. It is just a way I found to keep the file small and reuse as much code as possible, rather than rewriting the runtime 3 times (once for C, once for Metal, once for CUDA).
Don't know whether this is a common outcome, but I tried the "remove the walls" example, and the result was... scary. It completely changed the game so that movement is now diagonal, and made the arbitrary decision that up/down move you on the positive diagonal, and left/right move you on the negative diagonal.
The problem, of course, is that having only the one single "you can't win" law is severely underspecified, but the solution was too clever by half, and highlights the problem with this approach — every program will be under-specified, because, at some point, writing the laws becomes a bigger problem than writing the code itself.
This becomes a real issue because the combination of underspecified but rigid laws pushes the aI towards this sort of "creative" solution that matches the letter but not spirit of the law. In this case, the issue was obvious, but I seriously worry about what sort of shenanigans will occur in less obvious cases.
Exactly, "you can't win" is grossly under-specified. The goal of the demo is just to show that laws can't be broken. Yet, if that's your only law, the AI can do whatever to protect it - including changing how the character moves, or even removing the flag entirely!
So, yes, that's the issue with laws: they only protect what you remember to write. They're not a silver bullet. But they can still be incredibly useful, because it takes a small law to protect against entire classes of bug, covering your entire codebase. For example:
LAW: "the sum of all balances in this contract must be zero"
This one liner would have prevented Ethereum's infamous "The DAO" hack, where millions were stolen and almost undermined the entire project. But if your laws are under-specifying or ill-specifying your intents, Bend can't do anything to protect you.
Thought about automated discovery of laws in an existing codebase?
If you can find a law which the existing code obeys, and show it to a human, and if they agree, save it. And maybe the AI could make a decent guess as to what kind of laws would appeal to a human versus which wouldn't – a simple law identifying a fundamental constraint the system obeys is good, something really complicated or constraining something coincidentally true isn't
Or some kind of measure of coverage? you'd never want 100% – then your laws would become so complex you couldn't follow or maintain them – but if it is very low, that can be a signal to increase it
I think the premise is more that if one is given a grouping/constellation of unit tests that one can derive generalized laws by looking at what behavior those tests were checking for or against.
if there are a dozen unit tests trying to determine if some regex can escape a sensitive area, then one can derive a generalized 'don't let the regex escape from here' type rule -- or at least you could theoretically. I'm sure in reality that'd be a big minefield much like harness self-skill-writing has been.
From the codebases I have seen the "laws" are scattered between unit tests and lots of little tests and assertions in the actual code, plus cultural norms and "do it like this" patterns.
But a good start could be found in the unit tests.
What AI reviews? I thought AI needed to be bound by Bend laws.
The AI either knows what the user wants perfectly and is able to prevent problems, or is a rougue agent that needs to be bound by laws to not misbehave. You can't have both.
Well if possible you want an AI that understand the spirit of what you are asking for and will add all the missing stuff, instead of an AI that just want to hack its way to the result. Kinda what Fable brought to the table. For instance as a simple example I ask it to change the text that shows the email of the user by his name and Fable did all the code in case there is the family name missing etc. That this last part you want an AI to do. Helping you to build the system with you and not gaming what you ask for for reward.
Yeah all of these attempts to try and control AI outputs by using language fail to grasp that language is itself the problem. It is a closed system with no ground truth. Words only point to other words in an endless self-referential chain. There is no "closure" in language, ambiguity cannot be erased.
Imo LLM researchers would benefit a lot by reading what continental philosophers have said on the topic of language. Barthes, Sarte, Deluze, Derrida, et. Al have a lot to say that explains why we're running into the same problems over and over.
I think LLM researchers understand how LLMs work and what the limits of using natural language as an interface are. The problem is everyone else thinks they're basically magic, expecting them to be infinitely intuitive but also strictly deterministic, like the computer from Star Trek.
Plausibly based on what? The computer from Star Trek wasn't real. It was Majel Barrett talking into a microphone. You can no more extrapolate any real world computer architecture from that than you can determine amphibian biology from Kermit the Frog.
Fair enough. Your logic is unassailable. There is literally no difference between fiction and reality and no need to understand anything beyond "LLM talk therefore Star Trek real."
Right. Feel free to extrapolate a reading like "I think LLM tech and a century of tinkering could achieve computer performance similar to what it appears the entirely fictional, voiced by Majel Barrett, Star Trek computers has".
I got the same result when I tried the "remove the walls" example. I followed up by telling it to reimplement up/down/left/right movement without reinserting the walls and it basically made the square with the flag "unenterable". Like with a force field.
Respectfully I'm not sure if I share your worry though. You would have the same problem if you wrote extremely thorough / exhaustive unit tests or extremely precise types and didn't allow the LLM to amend them. You're basically shrinking the state space of what is considered a "correct" program per your spec. That the LLM has to get extremely creative to break your program is a _feature_; in my experience, an LLM does not have to get creative at all to break a typical program written in an enterprise setting, and that's unfortunate.
Side thought - I like the idea of this as a game, where you’re essentially fighting a monkeys paw / tricky genie. Not totally sure it’d work but I like the concept of trying not to get caught out.
Hey Victor! Been following you since HVM/Kind, partly because I'm moderately unhappy with the state of out of the box automatic parallelism in modern languages!
Do you plan to invest in profile guided optimization or autotuning in Bend2 - using runtime profiles / cost models to make decisions around SIMD vs. multicore vs. GPU parallelization?
Bend2's model might give you a really nice view into available parallelization. Heck I can imagine integrating an LLM to profile and optimize in an absurdly expensive `-O7` optimization mode one day!
Hi. Yes and of course, I plan to invest in everything that makes Bend better. The language is, in theory, capable of parallelizing perfectly in any setup. Currently, though, only a very simple scheduler is shipped, and you must still tune it manually. We're a small team, but we're not stopping here, and I hope I can make it grow to the point where that kind of tooling becomes part of the ecosystem.
Just wanted to say this is really, really cool, and impressive stuff. Looking forward to reading your papers and playing with it. Thanks for working hard on it and sharing it with us.
Sorry for not knowing, but in the AI world that we are in, I need to learn more about the creator behind a project to trust it. Something that can help me know why the creator is qualified to deliver on the promises being made, that I can trust their judgement and decision, that they know what they are doing and don't need AI to tell them what/how to do it, and that they are committed long term to the project. Do you think you could share a bit about you that would give me some answers on those?
This is really interesting, I’ve been very interested in the power of checks for code and things like hypothesis (which seem very similar in terms of writing a “for this kind of case, this holds true”, obviously different in terms of statistical checking vs actual proof).
I’ll have to explore and this isn’t my field so this isn’t a substantive comment and this may be bikeshedding but I found the game example a little confusing at first because we’d want winning to be possible. It fits the context of stopping a bad thing happening if it’s “evil actor can’t do X” and if your mind is on CTF but games we want to win.
Potential changes:
Make it a proof that the game can be won.
Make it require something first - so the game can’t be won unless the key is found for example. End result is still roughly the same and the failure case is still the same (walk over side of game) but it’s the kind of thing I’d want encoded in a puzzle game - game is winnable, but not winnable without getting the key first.
Since my other direction normally would be quickcheck style, I’d be interested in cases that are statistically hard to find but easy to prove exist. And in fairness, the other way too I guess. When to use each approach.
In the spirit of your comment, these are not things I see as failings, they are not things I in any way expect to be changed or done, they are intended as just an outsiders perspective if useful.
Thanks for making things, and thanks for releasing them!
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
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
Yes, there's a lot of vibe-coding in many places, but the critical parts (compiler, runtime, kernel) are human designed, and the kernel has been extensively audited by human. All of it is my own design and architecture, and I'm a human, I think. We'll prune AI slop over time. The project is big, and we're a small team.
1. The paper explains it well (sadly it is written by Claude for now, but it is accurate):
In short, we implemented a complete allocator, garbage-collector, closure evaluator and functional evaluator, on the GPU (with zero interaction net overhead this time). We then use a very simple (for now) scheduler that spreads binary recursive calls as to saturate all CPU or GPU cores, depending on where it is running. This is the simplest thing that works fast. In the future, we want to have a more flexible task stealing queue, but contention destroys GPU performance, so, that's the best thing that works, for now.
2. Benchmarks aside, large scale verified programs would run much faster on Bend for a simple reason: Bend is fully explicit. It has no tactics, and it does zero compile-time search. As always: the less a computer does, the faster it runs. This is a tradeoff. In exchange, Bend code is substantially more verbose than Lean, and it is more laborious to write Bend proofs. I argue this is the right tradeoff, because AI write proofs, and AI time is cheap, while bugs take human time, which is expensive.
3. Sorry I'm not proud of the commit history
4. I don't think it is worthy publication because the core idea is simple. We just use QTT-like linear types to fully prohibit runtime closures. So, paradoxes like Russel's and Girard's are blocked. In exchange, functions like List.map are not expressive (without templates). So it is not a research breakthrough. I just made a conscious trade here, which makes Bend way closer to C or Rust, than to Haskell or Lean.
5. Will patch.
Great questions actually, and surprisingly respectful. I appreciate it a lot.
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
2 isn't a big claim though, I think anyone developing Lean or Agda would agree these would be much faster with zero inference, unification or search? They'd just complain the language would become unergonomic, and that's true. Bend is very verbose.
Thanks and your feedbacks are reasonable, I appreciate
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
1. I do, but probably not in the current version, since I believe these proofs probably need full closure cloning to be ergonomic.
2. You can express anything actually, because you can clone data, just not functions. So, anything you could implement with datatypes (i.e., without cloned closures), you could probably also prove. But again, people use and abuse closure cloning a lot in Lean. So, how ergonomic would that be? I don't know. It is less about expressivity and more about ergonomics.
3. No, just in the runtime for now. Checking proofs on the GPU will happen when we implement Bend in itself.
You expect an arxiv only paper to be cited? Do you even know fuck all about scientific research? Do you think someone can slap "Foundations of" in an arxiv title and we are mandated to cite it?
before making slop accusations. Older variant of what became Bend is 5 years old, so definitely not "vibe coded": https://github.com/HigherOrderCO/HVM1
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
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.
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
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: https://bend-lang.com/bender
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.
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...
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?
> It sounds quite unlikely that a random vibecoded project with a Fable-written paper has worked out all of the kinks
> 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, but you are wildly overstating what you have here and sound sus af
These impute both his motives ("fun") and particularly his level of seriousness ("random vibecoded project" and "I like that you're interested in this area of research/engineering"—imputing passivity, as opposed to "are studying" or "are researching," which would be more appropriate given the amount of time invested).
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 negavity 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.)
In my culture it was ad personam, not even trying, and it’s fantastic that it’s been pointed out in a respectful way and reacted to with calm by all participants.
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. Since transparency builds trust, 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.
Maybe in our brave new world only the "laws" will matter and the implementation language is irrelevant to humans. In the mean time I have some questions about the "guide", which claims to define the entire language:
- There are no infinite loops, and recursion is kind of softly bounded to 2^48-1. This sounds grrrreat for games. I guess they have to stop working after a while? (What would be wrong with addressing this conceptually like Lean does? Have a way to annotate a term as possibly non-terminating?)
- We seem to have Data and Type and Kind, and they don't mean what they conventionally do. '-' means "used 0 types". And the example is:
def length(a, -A: Kind(a), xs: List<a, A>) -> Nat:
match xs:
case Nil{}:
0n
case Con{h, t}:
1n+length(a, A, t)
But wait! A is used albeit not at runtime. Is it possible that this actually intends "A may be used any number of times and is itself the name of a - type"? Shouldn't that be spelled "A: Kind(a) & -" or similar? Why does the kind even matter for this example?
- I don't understand the Array example:
import Base
def main() -> Array<U32> & U32:
a = [0 : U32*8n] # new array with 8 copies of 0
a[5] <- 42 # performs an in-place rewrite
a[5] # reads index 5
What is the return type of this function? It looks like it returns U32. So what's "Array<U32> & U32"?
- I don't even understand the Array explanation:
> The slot count after * is a power of two; [0 : U32^3n] names the depth instead.
Okay, the 8 in *8n above is indeed a power of two. Does the language require it? Does it actually mean 2^8? What is the "depth" of an array? Does this language not have non-power-of-two-sized arrays?
Nothing wrong with addressing it conceptually! We will, in the upcoming versions, probably via codata / coroutines. For V1, I'm keeping the language set smell. When it is stable, we'll add more features. Lean had 10+ years to mature; Bend is on day 1.
`-` means "erased argument". You can use an erased argument as many times as you want, in erased positions. That's also how QTT works (Idris2 is based on it). This example is there precisely to introduce Kinds, which are universes indexed on quantities.
- Kind(&2) is inhabited by clonable values.
- Kind(&1) is inhabited by linear values.
- Kind(&0) is like Rocq's Prop.
`A & B` is just sugar for the pair type former (which is sugar for a sigma).
So why does the length function take the ‘a’ parameter (the type of the elements?) and its Kind? Wouldn’t the type imply the kind? Why does the kind matter? Is the - a constraint on the kind? How would the program be different without the -?
When you say “pair type former” do you mean that Array<U32> & U32 is what Rust would call (Array<U32>, U32)? If so, why does that example function actually return a value of this type? It sure looks like it returns plain U32.
> You can use an erased argument as many times as you want, in erased positions.
What’s the rationale for this? Why is an “erased” position special? What is an erased position, anyway?
ISTM if I want to use an affine term that has zero size at runtime as a token that may be used at most once, I think I wouldn’t want an exception for using it in an “erased” position. Can I have a function like a -> a & a where the input is “erased”?
Oh, I see the confusion. That's bad syntax then. The 'a' parameter is not the type of the elements. It is the quantity of the Kind. This is similar to Agda's universe polymorphism. It is basically making the type of the list type polymorphic. It is a bit confusing, but it is there so you don't need to write List.length twice, one for copiable types, and another time for non-copiable types. Think of Rust generics; 'a' is playing the same role as a "Copiable" trait. It is an extra compile-time argument to avoid boilerplate.
Yes, `Array<U32> & U32` is just `(Array<U32>, U32)` and now that you point it I believe I made a bad syntactical choice here...
Also, `arr[3]` doesn't return a number. It returns the same array, and a number. I.e., if the element at index 3 is 123, then, `arr[3]` returns `(arr[3], 123)`. Now, you might be thinking: that's terrible. And yes, it is. I should probably have made the `arr[3]` syntax return 123. It exists for a very good reason though, it is what preserves linearity, so, this is part of the termination argument that makes Bend consistent. It was just an actual failure that I didn't anticipate people would react like that, and of course they would. I'll probably change that syntax. Sorry! I can see how confusing that example was.
Ohhh. Ok. I see the confusion. That's bad syntax then. The 'a' parameter is not the type of the elements. 'A' is the type of the elements. 'a' is just the "quantity of the type of the type of the elements". Yes, that's a mouthful, and somewhat abstract. This is similar to Agda's universe polymorphism. The reason it exists is because there are two "types of types" (i.e., kinds). Copiable types, and non-copiable types. So, this argument allows you to parametrize a function on both of these kinds. That way, you don't need to write List.length twice: one for copiable types, and once for non-copiable types. Think of Rust generics. 'a' is playing the same role as a "Copiable" trait would in Rust. It is just an extra compile-time argument to avoid boilerplate. But yes, I see how this can be confusing and I think I know how to improve that syntax.
Yes, `Array<U32> & U32` is just `(Array<U32>, U32)` and now that you point it I believe I made a bad choice, no excuses. Also, `arr[3]` doesn't return a number. It returns a copy of the same array, plus a number. So, if the element at index 3 is 123, tthen, `arr[3]` will return `(arr, 123)`. Now, you might be thinking: that's terrible. And yes, it is. I realize it now. I should have made the `arr[3]` syntax return 123. It is there for a very good reason though. It preserves linearity. It is part of the termination argument that makes Bend consistent. But yes, exposing it to the end user was most likely a mistake. I will redesign that syntax. Sorry about it.
The array thing is messy. It seems to me that there are potentially four kinds of arrays: the array itself can be copyable or not, and the contents can be copyable or not. But an array of copyable objects can be copied (possibly inefficiently depending what you're doing) whether the creator of the array wants you to or not, and a copyable array of noncopyable objects lets you copy the objects by copying the array. So maybe only two cases are really useful: when the copyability of the array matches the copyability of the objects.
In the everything-copyable case, you can just read an element.
In the nothing-copyable case, the syntax is irrelevant: the operation (arr, elem) = arr.read(index) is invalid.
If you want nice support for noncopyable arrays of noncopyable objects, you can do it Rust-style by having the ability to borrow the array, or you could have syntactical sugar for threading the array through a call, perhaps like:
arr#set(i, newvalue)
where the # syntax is sugar for:
arr = arr.set(i, newvalue)
(Yes, I know it's ugly. I'm not trying to win an aesthetic competition here.)
But this is at least a little bit messy because it forces the user to allow the method call to rebind the variable. Which is maybe not an actual problem -- Rust, for example, allows an &mut self method to swap self.
That being said, I think at least some Rust people wish that the ability to swap the referent of any &mut reference was not part of the language and was instead opt-in.
Claude Bopus has it for you. Its literally in the MCP. You should have harnesses with Sonneto. Have you even used the latest models? GPT Optimus have them.
Would the author have specified on the page that it's a fast new language with a new take on proof and so on, without mentioning ai and that alone would have caught my attention. It seems like if there isn't the word ai people are not interested anymore, we used to care many of us used to care
Everyone uses AI - yes me too. Everyone to code? I dunno know and no one actually know for sure. I find it more productive in many ways, not much for producing code, if not for highly verbose structured output. And I'd be interested in a new language polished to solve specific problems differently even if it doesn't mention ai. We did engineering for decades in this way
Unless the proofs themselves are defined with natural language, I don't see them being adopted by humans. It takes a high cognitive load to read let alone write a proof.
Sick of seeing "vibecoded!!" in the comments. It is an AI-oriented tool. Do you expect the author to write everything by hand? Do you think a couple of Claudeisms in the docs means the entire thing is unsupervised slop?
I'd love to know the true and honest statistics on how many professionals still write code by hand. If I were to guess, I'd say it's something like 10%.
I like the law idea, but what i found they end up doing is they just modify the law itself to fit the new feature they are working on, which defeats the point.
Which means some laws needs to be frozen. But not all laws, otherwise you can't add or modify anything. So the judgement is still on the human part, and we're back to meatbags being the bottleneck.
I've seen some success adding these proof-like checks to CI every time agents do something irrational. I definitely think it should be part of every codebase.
Yeah, you want to at least read what the AI is putting on LAWS.bend. It is substantially smaller than the codebase. Ultimately LAWS.bend makes you need to read astronomically less code. Not zero code.
I definitely think that's the approach going forward. We need to invest in things that increase the leverage of human attention on code verification. I've been thinking for a while that current unit tests frameworks don't have that good of a ratio
I read the readme and the guide file. There is just one thing I can comment: might as well solve the NP hard problems. I think you can do it easily, author. As you can already solved harder problems than those with your language.
> humans will eventually stop writing and reading code, but we still need an ambiguity-free way to tell the AIs building the world around us what we want done.
Why? Won't an AI that can correctly write any program (and make any change) also be smart enough to know what exactly we want better than we can explain, at least ahead-of-time?
> With proofs, we can verify that the AI implemented our prompts correctly.
How? Either we're able to understand all the theorems, which takes a lot of work, or we need to trust the AI, in which case the verification method can be a hidden implementation detail. Normally, when using formal methods, we choose to focus on certain important properties and verify only those.
I think that an AI that's smart enough to write almost any program and prove almost any property, will also be smart enough to not need to communicate with us formally and rather answer every question we have (and proofs are not always necessary, as they're not always necessary today), and probably also smart enough to figure out what we want built, and probably replace the software's users, too. I don't understand why it's likely that we'll have AI that's so capable to write all software correctly, yet not capable enough to do things that are probably easier.
An AI smart enough should act like a senior engineer gathering requirements, it should start with assumptions and poke at different areas with questions until it has a complete idea, when I talk with a client I dont expect him/her to really formalize all the details its my role to question them until all the sharp corners are covered
> Certainly such an AI would be able to just write machine code directly and verify it through whatever means, including formal proofs, as needed. Why does it need a compiler?
If the AI can write the program bytecode through AI magic, why can’t it verify that it works through AI magic?
The AI needs a compiler for the program for same reason it needs a proof language to verify it.
I realise most developers these days may have never written a program without a compiler (or an interpreter), but that is something we used to do. We'd write programs in Assembly. The AI won't even need the assembler. If verification is done through formal proofs, a logic language is, indeed, needed, but the program itself could remain in machine code.
We did used to write programs that way, but as the programs (and machines) got larger and more complicated, we found it very hard to so we invented all kinds of languages and abstractions to help us think about programs.
Why would an advanced intelligence be able to think about the large programs without similar tools?
Moreover, why do you believe the AI will be able to write the program without special languages, but that it would still need a special language to verify the program? That’s the gap I’m not understanding.
Machine code is a special language for programming, and since this is an exercise in imagining what an AI that could do anything would do, I don't see why it would need anything else. Machine code, however, follows the rules of a computer and not of those of a predicate logic, hence another language is needed for proofs.
But if it needs one language for programming, machine code, why is that the optimal and only one for every application? There’s not even one machine code, it’s per machine and each one has their own design constraints and quirks. Why should all semantic reasoning be duplicated separately at each machine-code level rather than factoring common meaning above those targets and proving that the target-specific lowerings preserve it?
Also predicate logic can be expressed using machine code, so why does the AI need a whole other notation to express predicate logic? It should just be able to use whatever machine code it used to write the program.
If the answer is that the verifier would benefit from extra semantic information in the logic language, then why doesn’t that same representational argument apply to programs? Programs also have semantic structures that aren’t naturally expressed by the ISA. E.g. types, effects, state machines, matrix operations, synchronization, ownership, capabilities, protocols, etc.
Moreover, why can’t this hypothetical AI just write correct code that doesn’t need to be proved through predicate logic?
> If for some reason an AI capable of writing and proving arbitrary programs thinks it will be aided by a compiler, surely it will be able to create its own ad-hoc one for the problem at hand.
I think this basically concedes my point: you’re saying the ai will create ad hoc programming languages to support its thinking, which I think is much closer to what will happen. I think it would choose to do this in nearly all cases. It’s one thing to be able to prove arbitrary programs, quite another to do so within resource constraints, like finishing the proof before the heat death of the universe.
Take for instance this expression:
A * B
Where A and B are matrices and * is matrix multiply.
The most efficient machine code for this will unroll all of the loops and multiplications and additions, pipeline and fuse them, and schedule them across parallel registers for SIMD instruction.
The machine code instructions to express just this one instance would be hundreds to thousands of bytes depending on the size of the matrix.
What’s easier: verifying the high-level matrix multiply to Machine Code lowering is correct (per machine) and therefore every application of it is correct; or that every single bespoke matrix multiply is a correct instance for every machine?
At some level you’d spend more time proving every instance of bespoke unrolled matrix multiply machine code every time you generate it than just generating a permanent deterministic compiler and using that instead. I think a sufficiently smart AI would figure this out and absolutely take that shortcut, for the same reasons humans did.
The prover itself benefits from establishing higher level concepts as well, so there’s a real disconnect between the predicate logic and the machine code. The verifier would thrive on semantic information like: the matrix dimensions are fixed, the dimensions are compatible, the types are consistent, the values are immutable… all of that is intentionally missing by the time you lower to machine code (usually because it’s usefulness in proving the program have been exhausted).
Removing all that semantic information leaves the prover having to reinvent it on every proof. So I guess you could include that higher level semantic information in the machine code but now you’re back to designing a programming language.
> But if it needs one language for programming, machine code, why is that the optimal and only one for every application?
Why would any other specific language be? Machine code is the most general and, as I said, if the AI wants to use a compiler to, say, help generate code for other platforms, it can create one.
> Also predicate logic can be expressed using machine code
It can't. Predicate logic has certain deduction rules, and these rules are different from those of machine code (e.g. machine code doesn't have quantifiers or their introduction and elimination rules). Of course, the AI could invent an ad hoc logic language and write a prover for it, but in this thought exercise, I think the point is that people would want to verify the proven properties (and possibly the implementation of the proof checker).
> What’s easier: verifying the high-level matrix multiply to machine code lowering is correct (per machine) and therefore every application of it is correct; or that every single bespoke matrix multiply actually correctly implements matrix multiply for every machine?
This isn't too relevant. If you need to build a skyscraper for tens of millions of dollars, you wouldn't spend much time thinking about how to lower the cost of the handle on the front entrance by $10. Even if every matrix multiplication is a little different, the proofs can be copied and changed slightly. The difference in cost of doing that or not is negligible compared to other aspects of the verification. Again, we write programs that are three orders of magnitude larger than the largest program we've ever managed to prove correct, and the difficulty does not scale linearly. So we're talking about an AI that's 10,000 or 100,000 times more capable than humans at writing software. Surely, matters as duplicating code and proofs are negligible for it.
But even if it does matter, machine code isn't a problem because you don't have to duplicate manually. You can write the machine code that specialises the different applications and prove the correctness of that. This is like writing a small portion of a compiler.
My general point is that proving arbitrary (practical) correctness properties of arbitrary (practical) programs is such a monumental achievement that anything more mundane, like a compiler, is trivial in comparison.
“but we still need an ambiguity-free way to
tell the AIs building the world around us what we want done”
Do we? I would argue one of the main reasons AI can be so productive is because it makes assumptions where it finds ambiguity, and we reduce the number of things we need to specify.
339 comments
[ 4.6 ms ] story [ 216 ms ] threadit is not a pretty file and it has a lot of gambiarra and AI slop for now
if you want to read something worthy, read the kernel (bend.ts)
I had to look up "gambiarra": a Brazilian expression that means to use improvised methods to solve a problem with any avaiable material.
Totally understandable, I think you did the right thing by releasing early, even if it's still in rough shape, to get some public feedback. This forum can be a hit-or-miss, sometimes even great projects are not appreciated (and the opposite too). But I imagine some people are in the target audience who will see the project and actually explore the language, and follow along with its development.
[1] https://hdl.handle.net/10779/uos.32024301
...did they just squash the repo to 1 commit for v2.0.4? Why? Yall should know that in this age of AI trust is the real currency... and nuking your history is one hell of a way to raise eyebrows.
> Enjoy bug-free, fast vibe-coded apps! Hints: ask it to write laws for whatever should never break, and to parallelize everything you want running fast. Bend is young: if anything goes wrong, ask it to open an issue.
Emphasis mine. I don't want to be snarky but like... come on.
...so now their work has been reduced to nothing?
is this a problem to you? why
Virtually everyone has AI slop in the commit history. No one's judging you for the commit history. Everyone's code smells, but the fact that you're ashamed/hiding it is... odd.
> there's a lot of personal info
You should know that force pushing doesn't hide actual commits; it's trivially viewable if someone just iterates https://github.com/bendlang/bend/activity?ref=main e.g. https://github.com/bendlang/bend/commit/d184863 so like... why bother.
https://github.com/bendlang/bend/blob/80b6539bc57621633ca68e...
Hmmm... needs `sudo`.
One time they force pushed and erased everything except a 2-line README... on purpose.
Pre-obliteration version: https://github.com/bendlang/bend/tree/814453670d0e0d6777c131...
It's too difficult and doesn't scale well to many real world programs - how do you formally verify Facebook?
We'll probably be stuck with normal testing and at least skimming code for a while.
https://aws.amazon.com/blogs/compute/aws-nitro-isolation-eng...
And for the PQ parts of Apple's crypto libraries, from May:
https://security.apple.com/blog/formal-verification-corecryp...
Similar from Microsoft, from July:
https://www.microsoft.com/en-us/research/blog/verifying-rust...
Robots are logical, but not rational.
What they aren't is moral, because of the orthogonality principle: you can't use facts and logic to discover correct moral beliefs. Morality is about values, goals, and the definition of "good". They must be provided to the robot by its creator, and those are things that are very hard to precisely describe in a way that is fully consistent with the speaker's intent in all possible scenarios, and agreeable by all other people.
I take it you haven't used Microsoft Windows?
Joking, joking...
They asked a computer how to minimize production expenses at a factory. The computer said: "Do not manufacture anything, expenses will be zero".
I believe it's been around since expert systems at least.
HN staff: someone posted before me. Could we change the title to "Bend - a language that blocks AI mistakes via proof and runs on GPUs"?
Everyone: feel free to ask any question, but I'd be highly appreciative if you could be a bit civilized and respectful this time. I've worked on this for 1 year, nearly 16h/day, 7 days a week, and I'm giving it for free. You need not to use it. So, I'd be thankful if you could point occasional failures politely rather than throwing me in a lava pit.
Thank you!
I'm confused - could you explain how the board/flag animation relates to Bend's compile time checking? Is it actually a direct demonstration of Bend running a check?
(Why it is done the way it is, what problems are solved by affinity, why closure can be called at most once, how a function that never returns can prove anything, and everything else)
If you mean about the type theory specifically, "Type Theory and Formal Proof by Nederpelt and Geuvers" is a good introduction. Not sure what I'd recommend on linear types, no book I know of is very introductory? Perhaps "Idris 2: Quantitative Type Theory in Practice", which is a language with similar foundations to Bend, and the author wrote a book on it (and inspired myself!)
> That same file is the CPU program and the GPU kernel: clang builds it for the host, Metal or CUDA builds it for the device, so a `!` runs the exact same code on either chip.
What exactly is this saying? The guide doesn't really explicitly define `!`, and it's unclear from this sentence whether it's saying that, "clang builds it for the host and Metal, and CUDA builds it for the device", or if it's saying, "clang builds it for the host, Metal, and CUDA, and builds it for the device", or something else entirely.
It just means that Bend compiles to a single .c file, and that file compiles to either Metal or CUDA, via macros, depending on your target. This shouldn't be relevant to most users. It is just a way I found to keep the file small and reuse as much code as possible, rather than rewriting the runtime 3 times (once for C, once for Metal, once for CUDA).
The problem, of course, is that having only the one single "you can't win" law is severely underspecified, but the solution was too clever by half, and highlights the problem with this approach — every program will be under-specified, because, at some point, writing the laws becomes a bigger problem than writing the code itself.
This becomes a real issue because the combination of underspecified but rigid laws pushes the aI towards this sort of "creative" solution that matches the letter but not spirit of the law. In this case, the issue was obvious, but I seriously worry about what sort of shenanigans will occur in less obvious cases.
So, yes, that's the issue with laws: they only protect what you remember to write. They're not a silver bullet. But they can still be incredibly useful, because it takes a small law to protect against entire classes of bug, covering your entire codebase. For example:
LAW: "the sum of all balances in this contract must be zero"
This one liner would have prevented Ethereum's infamous "The DAO" hack, where millions were stolen and almost undermined the entire project. But if your laws are under-specifying or ill-specifying your intents, Bend can't do anything to protect you.
If you can find a law which the existing code obeys, and show it to a human, and if they agree, save it. And maybe the AI could make a decent guess as to what kind of laws would appeal to a human versus which wouldn't – a simple law identifying a fundamental constraint the system obeys is good, something really complicated or constraining something coincidentally true isn't
Or some kind of measure of coverage? you'd never want 100% – then your laws would become so complex you couldn't follow or maintain them – but if it is very low, that can be a signal to increase it
They are usually in the “tests” folder.
So anything capable of extracting unit tests is extracting “laws”.
One might consider the test name the text of a law. And the AI fills in the details.
Unit tests check whether a specific code module is implemented correctly given its (implicit) specification.
Good “laws” are independent of the structure of the code.
Tests may be a useful source for inferring what the laws are, but much of the actual content of the tests aren’t “laws” at all.
if there are a dozen unit tests trying to determine if some regex can escape a sensitive area, then one can derive a generalized 'don't let the regex escape from here' type rule -- or at least you could theoretically. I'm sure in reality that'd be a big minefield much like harness self-skill-writing has been.
But a good start could be found in the unit tests.
What prevents AI from writing an arbitrary calculation that makes sure that sum is always zero while breaking a whole other bunch of assumptions?
If the answer is more laws, then this does not address the parent comment.
The AI either knows what the user wants perfectly and is able to prevent problems, or is a rougue agent that needs to be bound by laws to not misbehave. You can't have both.
But that's how it is anyway, no?
Defining clear boundaries and clear goals is the hardest part. If you get those right everything else is rather trivial.
Imo LLM researchers would benefit a lot by reading what continental philosophers have said on the topic of language. Barthes, Sarte, Deluze, Derrida, et. Al have a lot to say that explains why we're running into the same problems over and over.
I actually think Asimov is more instructive here, while Gödel and Tarski tell us the tool can’t prove itself…
Nonetheless, it is a worthwhile endeavor and I hope more rigorous practices like this catch on.
Respectfully I'm not sure if I share your worry though. You would have the same problem if you wrote extremely thorough / exhaustive unit tests or extremely precise types and didn't allow the LLM to amend them. You're basically shrinking the state space of what is considered a "correct" program per your spec. That the LLM has to get extremely creative to break your program is a _feature_; in my experience, an LLM does not have to get creative at all to break a typical program written in an enterprise setting, and that's unfortunate.
Do you plan to invest in profile guided optimization or autotuning in Bend2 - using runtime profiles / cost models to make decisions around SIMD vs. multicore vs. GPU parallelization?
Bend2's model might give you a really nice view into available parallelization. Heck I can imagine integrating an LLM to profile and optimize in an absurdly expensive `-O7` optimization mode one day!
É ótimo ver um brasileiro criando algo tão único!
https://gist.github.com/VictorTaelin/77fd5a2a8a4a07e1da6157e...
https://github.com/victortaelin
Cool project!
This is really interesting, I’ve been very interested in the power of checks for code and things like hypothesis (which seem very similar in terms of writing a “for this kind of case, this holds true”, obviously different in terms of statistical checking vs actual proof).
I’ll have to explore and this isn’t my field so this isn’t a substantive comment and this may be bikeshedding but I found the game example a little confusing at first because we’d want winning to be possible. It fits the context of stopping a bad thing happening if it’s “evil actor can’t do X” and if your mind is on CTF but games we want to win.
Potential changes:
Make it a proof that the game can be won.
Make it require something first - so the game can’t be won unless the key is found for example. End result is still roughly the same and the failure case is still the same (walk over side of game) but it’s the kind of thing I’d want encoded in a puzzle game - game is winnable, but not winnable without getting the key first.
Since my other direction normally would be quickcheck style, I’d be interested in cases that are statistically hard to find but easy to prove exist. And in fairness, the other way too I guess. When to use each approach.
In the spirit of your comment, these are not things I see as failings, they are not things I in any way expect to be changed or done, they are intended as just an outsiders perspective if useful.
Thanks for making things, and thanks for releasing them!
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
1. The paper explains it well (sadly it is written by Claude for now, but it is accurate):
https://github.com/bendlang/bend/blob/main/paper/BendRT.pdf
In short, we implemented a complete allocator, garbage-collector, closure evaluator and functional evaluator, on the GPU (with zero interaction net overhead this time). We then use a very simple (for now) scheduler that spreads binary recursive calls as to saturate all CPU or GPU cores, depending on where it is running. This is the simplest thing that works fast. In the future, we want to have a more flexible task stealing queue, but contention destroys GPU performance, so, that's the best thing that works, for now.
2. Benchmarks aside, large scale verified programs would run much faster on Bend for a simple reason: Bend is fully explicit. It has no tactics, and it does zero compile-time search. As always: the less a computer does, the faster it runs. This is a tradeoff. In exchange, Bend code is substantially more verbose than Lean, and it is more laborious to write Bend proofs. I argue this is the right tradeoff, because AI write proofs, and AI time is cheap, while bugs take human time, which is expensive.
3. Sorry I'm not proud of the commit history
4. I don't think it is worthy publication because the core idea is simple. We just use QTT-like linear types to fully prohibit runtime closures. So, paradoxes like Russel's and Girard's are blocked. In exchange, functions like List.map are not expressive (without templates). So it is not a research breakthrough. I just made a conscious trade here, which makes Bend way closer to C or Rust, than to Haskell or Lean.
5. Will patch.
Great questions actually, and surprisingly respectful. I appreciate it a lot.
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
Thanks and your feedbacks are reasonable, I appreciate
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
2. You can express anything actually, because you can clone data, just not functions. So, anything you could implement with datatypes (i.e., without cloned closures), you could probably also prove. But again, people use and abuse closure cloning a lot in Lean. So, how ergonomic would that be? I don't know. It is less about expressivity and more about ergonomics.
3. No, just in the runtime for now. Checking proofs on the GPU will happen when we implement Bend in itself.
I suggest you read his history: 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": https://github.com/HigherOrderCO/HVM1
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
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 : https://github.com/VictorTaelin/Interaction-Type-Theory that's 3 year old, pre-dates Fable, but OMG doesn't look like a paper.
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
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: https://bend-lang.com/bender
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.
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...
Have you evaluated it?
Wouldn’t you be inclined to withhold any claims of anything being substantiated until it’s actually been evaluated?
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?
Are you arguing with me or the parent who actually called it “sus af”?
> It sounds quite unlikely that a random vibecoded project with a Fable-written paper has worked out all of the kinks
> 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, but you are wildly overstating what you have here and sound sus af
These impute both his motives ("fun") and particularly his level of seriousness ("random vibecoded project" and "I like that you're interested in this area of research/engineering"—imputing passivity, as opposed to "are studying" or "are researching," which would be more appropriate given the amount of time invested).
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 negavity 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.)
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”.
The author was very polite to even reply at all.
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. Since transparency builds trust, 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.
https://github.com/bendlang/bend/blob/main/guide/GUIDE.md
Let's see:
- There are no infinite loops, and recursion is kind of softly bounded to 2^48-1. This sounds grrrreat for games. I guess they have to stop working after a while? (What would be wrong with addressing this conceptually like Lean does? Have a way to annotate a term as possibly non-terminating?)
- We seem to have Data and Type and Kind, and they don't mean what they conventionally do. '-' means "used 0 types". And the example is:
But wait! A is used albeit not at runtime. Is it possible that this actually intends "A may be used any number of times and is itself the name of a - type"? Shouldn't that be spelled "A: Kind(a) & -" or similar? Why does the kind even matter for this example?- I don't understand the Array example:
What is the return type of this function? It looks like it returns U32. So what's "Array<U32> & U32"?- I don't even understand the Array explanation:
> The slot count after * is a power of two; [0 : U32^3n] names the depth instead.
Okay, the 8 in *8n above is indeed a power of two. Does the language require it? Does it actually mean 2^8? What is the "depth" of an array? Does this language not have non-power-of-two-sized arrays?
At this point I stopped reading.
`-` means "erased argument". You can use an erased argument as many times as you want, in erased positions. That's also how QTT works (Idris2 is based on it). This example is there precisely to introduce Kinds, which are universes indexed on quantities.
- Kind(&2) is inhabited by clonable values. - Kind(&1) is inhabited by linear values. - Kind(&0) is like Rocq's Prop.
`A & B` is just sugar for the pair type former (which is sugar for a sigma).
Thanks for your questions and patience!
When you say “pair type former” do you mean that Array<U32> & U32 is what Rust would call (Array<U32>, U32)? If so, why does that example function actually return a value of this type? It sure looks like it returns plain U32.
> You can use an erased argument as many times as you want, in erased positions.
What’s the rationale for this? Why is an “erased” position special? What is an erased position, anyway?
ISTM if I want to use an affine term that has zero size at runtime as a token that may be used at most once, I think I wouldn’t want an exception for using it in an “erased” position. Can I have a function like a -> a & a where the input is “erased”?
Yes, `Array<U32> & U32` is just `(Array<U32>, U32)` and now that you point it I believe I made a bad syntactical choice here...
Also, `arr[3]` doesn't return a number. It returns the same array, and a number. I.e., if the element at index 3 is 123, then, `arr[3]` returns `(arr[3], 123)`. Now, you might be thinking: that's terrible. And yes, it is. I should probably have made the `arr[3]` syntax return 123. It exists for a very good reason though, it is what preserves linearity, so, this is part of the termination argument that makes Bend consistent. It was just an actual failure that I didn't anticipate people would react like that, and of course they would. I'll probably change that syntax. Sorry! I can see how confusing that example was.
Yes, `Array<U32> & U32` is just `(Array<U32>, U32)` and now that you point it I believe I made a bad choice, no excuses. Also, `arr[3]` doesn't return a number. It returns a copy of the same array, plus a number. So, if the element at index 3 is 123, tthen, `arr[3]` will return `(arr, 123)`. Now, you might be thinking: that's terrible. And yes, it is. I realize it now. I should have made the `arr[3]` syntax return 123. It is there for a very good reason though. It preserves linearity. It is part of the termination argument that makes Bend consistent. But yes, exposing it to the end user was most likely a mistake. I will redesign that syntax. Sorry about it.
In the everything-copyable case, you can just read an element.
In the nothing-copyable case, the syntax is irrelevant: the operation (arr, elem) = arr.read(index) is invalid.
If you want nice support for noncopyable arrays of noncopyable objects, you can do it Rust-style by having the ability to borrow the array, or you could have syntactical sugar for threading the array through a call, perhaps like:
where the # syntax is sugar for: (Yes, I know it's ugly. I'm not trying to win an aesthetic competition here.)But this is at least a little bit messy because it forces the user to allow the method call to rebind the variable. Which is maybe not an actual problem -- Rust, for example, allows an &mut self method to swap self.
That being said, I think at least some Rust people wish that the ability to swap the referent of any &mut reference was not part of the language and was instead opt-in.
Why would anyone want to work with such a dystopian setup? Prove your code directly in Lean or Coq or leave it.
I like the law idea, but what i found they end up doing is they just modify the law itself to fit the new feature they are working on, which defeats the point.
Which means some laws needs to be frozen. But not all laws, otherwise you can't add or modify anything. So the judgement is still on the human part, and we're back to meatbags being the bottleneck.
I've seen some success adding these proof-like checks to CI every time agents do something irrational. I definitely think it should be part of every codebase.
There's also https://code-contracts.cc/ which co-locates code and proofs together.
Question, does the parallelism work on M-Series GPU? The page says CUDA parallelism but shows Mac performance numbers.
Currently, parallelism works in any multi-core CPU, and in Apple M-series and NVIDIA GPUs.
I will later. From what I can tell it looks nice. I like the syntax. I don’t know of the claims but willing to give it a shot.
The GPU story would it work on my Mac or is it not GPU agnostic?
Got it to port kaparthys microgpt -> https://github.com/thomasdavis/bend-experiments/tree/main/mi...
muse did surprisingly well getting it to work, can't speak for the code quality.
Welcome to HN!
May I remind you of the Dropbox comment? https://news.ycombinator.com/item?id=9224
Why? Won't an AI that can correctly write any program (and make any change) also be smart enough to know what exactly we want better than we can explain, at least ahead-of-time?
> With proofs, we can verify that the AI implemented our prompts correctly.
How? Either we're able to understand all the theorems, which takes a lot of work, or we need to trust the AI, in which case the verification method can be a hidden implementation detail. Normally, when using formal methods, we choose to focus on certain important properties and verify only those.
I think that an AI that's smart enough to write almost any program and prove almost any property, will also be smart enough to not need to communicate with us formally and rather answer every question we have (and proofs are not always necessary, as they're not always necessary today), and probably also smart enough to figure out what we want built, and probably replace the software's users, too. I don't understand why it's likely that we'll have AI that's so capable to write all software correctly, yet not capable enough to do things that are probably easier.
If the AI can write the program bytecode through AI magic, why can’t it verify that it works through AI magic?
The AI needs a compiler for the program for same reason it needs a proof language to verify it.
Why would an advanced intelligence be able to think about the large programs without similar tools?
Moreover, why do you believe the AI will be able to write the program without special languages, but that it would still need a special language to verify the program? That’s the gap I’m not understanding.
Also predicate logic can be expressed using machine code, so why does the AI need a whole other notation to express predicate logic? It should just be able to use whatever machine code it used to write the program.
If the answer is that the verifier would benefit from extra semantic information in the logic language, then why doesn’t that same representational argument apply to programs? Programs also have semantic structures that aren’t naturally expressed by the ISA. E.g. types, effects, state machines, matrix operations, synchronization, ownership, capabilities, protocols, etc.
Moreover, why can’t this hypothetical AI just write correct code that doesn’t need to be proved through predicate logic?
> If for some reason an AI capable of writing and proving arbitrary programs thinks it will be aided by a compiler, surely it will be able to create its own ad-hoc one for the problem at hand.
I think this basically concedes my point: you’re saying the ai will create ad hoc programming languages to support its thinking, which I think is much closer to what will happen. I think it would choose to do this in nearly all cases. It’s one thing to be able to prove arbitrary programs, quite another to do so within resource constraints, like finishing the proof before the heat death of the universe.
Take for instance this expression:
A * B
Where A and B are matrices and * is matrix multiply.
The most efficient machine code for this will unroll all of the loops and multiplications and additions, pipeline and fuse them, and schedule them across parallel registers for SIMD instruction.
The machine code instructions to express just this one instance would be hundreds to thousands of bytes depending on the size of the matrix.
What’s easier: verifying the high-level matrix multiply to Machine Code lowering is correct (per machine) and therefore every application of it is correct; or that every single bespoke matrix multiply is a correct instance for every machine?
At some level you’d spend more time proving every instance of bespoke unrolled matrix multiply machine code every time you generate it than just generating a permanent deterministic compiler and using that instead. I think a sufficiently smart AI would figure this out and absolutely take that shortcut, for the same reasons humans did.
The prover itself benefits from establishing higher level concepts as well, so there’s a real disconnect between the predicate logic and the machine code. The verifier would thrive on semantic information like: the matrix dimensions are fixed, the dimensions are compatible, the types are consistent, the values are immutable… all of that is intentionally missing by the time you lower to machine code (usually because it’s usefulness in proving the program have been exhausted).
Removing all that semantic information leaves the prover having to reinvent it on every proof. So I guess you could include that higher level semantic information in the machine code but now you’re back to designing a programming language.
Why would any other specific language be? Machine code is the most general and, as I said, if the AI wants to use a compiler to, say, help generate code for other platforms, it can create one.
> Also predicate logic can be expressed using machine code
It can't. Predicate logic has certain deduction rules, and these rules are different from those of machine code (e.g. machine code doesn't have quantifiers or their introduction and elimination rules). Of course, the AI could invent an ad hoc logic language and write a prover for it, but in this thought exercise, I think the point is that people would want to verify the proven properties (and possibly the implementation of the proof checker).
> What’s easier: verifying the high-level matrix multiply to machine code lowering is correct (per machine) and therefore every application of it is correct; or that every single bespoke matrix multiply actually correctly implements matrix multiply for every machine?
This isn't too relevant. If you need to build a skyscraper for tens of millions of dollars, you wouldn't spend much time thinking about how to lower the cost of the handle on the front entrance by $10. Even if every matrix multiplication is a little different, the proofs can be copied and changed slightly. The difference in cost of doing that or not is negligible compared to other aspects of the verification. Again, we write programs that are three orders of magnitude larger than the largest program we've ever managed to prove correct, and the difficulty does not scale linearly. So we're talking about an AI that's 10,000 or 100,000 times more capable than humans at writing software. Surely, matters as duplicating code and proofs are negligible for it.
But even if it does matter, machine code isn't a problem because you don't have to duplicate manually. You can write the machine code that specialises the different applications and prove the correctness of that. This is like writing a small portion of a compiler.
My general point is that proving arbitrary (practical) correctness properties of arbitrary (practical) programs is such a monumental achievement that anything more mundane, like a compiler, is trivial in comparison.
Do we? I would argue one of the main reasons AI can be so productive is because it makes assumptions where it finds ambiguity, and we reduce the number of things we need to specify.