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.
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.
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.
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).
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!
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?
The check is happening in between the animations. When the AI edits the code, Bend will check if all laws still hold, mathematically so. If not, the AI repeats, until that's the case. So, the animations just show what happens to the app with and without Bend's involvement.
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!)
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.
I think this is premise for AI: Lean and formal verification seems more and more important in today's world and I think a variation of programming language like this is bound to win. This, or a library or framework to prove typescript.
Cool idea. I tried using it to port a little meeting fixer cron job I vibe coded, it seemed a natural fit as its essentially trying to satisfy invariants in my calendar.
It basically succeeded but Claude (Opus 5) did have some complaints:
'Base ships one arithmetic law, U32.add_comm. There is no order theory. About 60 of PROOF.bend's 163 lines are cmp_refl, and_false, and_comm, le_max_l, le_max_r, add_succ — facts you'd assume exist. You'd write them once per project and never again, but budget for them.'
'Base's Nat.max is unusable in a proof. It's Bool.pick(Nat, Nat.is_lt(a,b), b, a), and a proof can't case on a computed value. I wrote a structurally recursive nat_max so it unfolds in lockstep with Nat.cmp.'
'The law I most wanted: "no two output plans overlap." I didn't state it. It needs the sortedness of collapse's input as a hypothesis, and Base's List.sort ships no sortedness law — so getting there means proving merge sort correct first. That's the honest measure of the gap between "provable in principle" and "provable this afternoon."'
I've got basically a minor in CS so I'm a dummy when it comes to proofs. I don't know if this is valuable feedback or simply Claude misunderstanding something.
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.
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.
I’m missing an actual explanation of how that works.
I feel like we all had the idea, but how is all possible move sequences proven ?
What if the possible scenarios are too big to proof or test.
Like on a 2 dimensional game it’s easy, but you could make it multidimensional and introduce an unlimited amount of special rules, (if on a prime number dimension on 3 but not more prime numbers you are allowed to jump to another prime numbers with 3 but not less coordinates)
How is bend protecting it? I was checkin github and the paper, but I was not motivated enough. I feel like an actual explanation of how proofing works is missing.
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
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.
So sad that commit history is a thing we can feel emotionally attached to a point of feeling vulnerable when releasing it with others.
Also equally sad that without a way to relate easily with how something came to be (e.g. the commit history) others will struggle focusing at the work and will judge its lineage.
I guess to folks here confused by that go search SrPeixinho on Reddit and that should have a lot of history for you to understand the background of the work, and you can also join their Discord server and literally talk to them there.
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.
Agree, but natural languages have ambiguity, the AI output should really include the assumptions and we seriously need to replace the word "prompt" with "conversation".
I think a big issue we keep running into is this idea that language is ambiguous but code is somehow not. Code is merely an extension of language, a DSL if you will. Implicit assumptions become baked into the logic of the code and those assumptions can be wrong.
Look at the guy whose AI changed the entire rules of the game to avoid breaking the law. Was that really the desired outcome? And the more you try to lock it down the more language you add and therefore more ambiguity and assumptions.
You cannot solve the problems of language with more language.
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
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
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?
Yes, I'd expect a 2 year old preprint from a rising research in this utlra-niche field to likely be discussed when someone is claiming to have a sweeping solution on exactly the same research question
Maybe not necessarily so, but while looking through the paper's bibliography I get the sense that these were AI-gathered references because there seems to be gaps in the current literature on this topic
> In the post-AGI economy, 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?
If AGI means "human level", why is there any part of the process that humans will be needed for, especially some engineering aspect?
> With proofs, we can verify that the AI implemented our prompts correctly.
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?
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. It's probably capable enough to 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
Yes, but also, who do you gather requirements from? Other people. But if we're talking AGI, then these other people, i.e. users - or at least those who define the requirements - could be replaced, too.
“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.
...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.
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?
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.
Hmmm. I don’t really have any issues with frontier models not implementing my prompts correctly, and presumably that will only become more and more the case as the models get better and better. This seems like almost a non-issue already and certainly on its way to becoming one for sure?
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”?
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.
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?
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!
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.
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.
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.
Of course because at its limit programming is basically defining desired behaviour under all circumstances and logical conditions.
I wonder if harness-hooks + Jev (equivalents) could semantically lint for `sloppy_law` etc when ever they are edited
> 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).
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!)
É ótimo ver um brasileiro criando algo tão único!
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!
You can find it on Bend's demo directory in our GitHub.
Don't tell anyone though!
https://benjdd.com/languages/
It basically succeeded but Claude (Opus 5) did have some complaints:
'Base ships one arithmetic law, U32.add_comm. There is no order theory. About 60 of PROOF.bend's 163 lines are cmp_refl, and_false, and_comm, le_max_l, le_max_r, add_succ — facts you'd assume exist. You'd write them once per project and never again, but budget for them.'
'Base's Nat.max is unusable in a proof. It's Bool.pick(Nat, Nat.is_lt(a,b), b, a), and a proof can't case on a computed value. I wrote a structurally recursive nat_max so it unfolds in lockstep with Nat.cmp.'
'The law I most wanted: "no two output plans overlap." I didn't state it. It needs the sortedness of collapse's input as a hypothesis, and Base's List.sort ships no sortedness law — so getting there means proving merge sort correct first. That's the honest measure of the gap between "provable in principle" and "provable this afternoon."'
I've got basically a minor in CS so I'm a dummy when it comes to proofs. I don't know if this is valuable feedback or simply Claude misunderstanding something.
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.
I feel like we all had the idea, but how is all possible move sequences proven ?
What if the possible scenarios are too big to proof or test.
Like on a 2 dimensional game it’s easy, but you could make it multidimensional and introduce an unlimited amount of special rules, (if on a prime number dimension on 3 but not more prime numbers you are allowed to jump to another prime numbers with 3 but not less coordinates)
How is bend protecting it? I was checkin github and the paper, but I was not motivated enough. I feel like an actual explanation of how proofing works is missing.
For Lean I understand how it works, here not.
[1] https://hdl.handle.net/10779/uos.32024301
Also equally sad that without a way to relate easily with how something came to be (e.g. the commit history) others will struggle focusing at the work and will judge its lineage.
I guess to folks here confused by that go search SrPeixinho on Reddit and that should have a lot of history for you to understand the background of the work, and you can also join their Discord server and literally talk to them there.
Look at the guy whose AI changed the entire rules of the game to avoid breaking the law. Was that really the desired outcome? And the more you try to lock it down the more language you add and therefore more ambiguity and assumptions.
You cannot solve the problems of language with more language.
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
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
Maybe not necessarily so, but while looking through the paper's bibliography I get the sense that these were AI-gathered references because there seems to be gaps in the current literature on this topic
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?
If AGI means "human level", why is there any part of the process that humans will be needed for, especially some engineering aspect?
> With proofs, we can verify that the AI implemented our prompts correctly.
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?
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. It's probably capable enough to 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.
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.
...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.
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...
Hmmm... needs `sudo`.
...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.
Scam detected.
Where are those benchmarks and how do I reproduce them ?
The script we use to run them on our servers: https://github.com/bendlang/bend/blob/main/gates/perf.ts
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”?
Question, does the parallelism work on M-Series GPU? The page says CUDA parallelism but shows Mac performance numbers.
it 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 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?
Why would anyone want to work with such a dystopian setup? Prove your code directly in Lean or Coq or leave it.
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...