Bend – a language that blocks AI mistakes via proof and runs on GPUs
bend-lang.com
bend-lang.com
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.
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.
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.
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.
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
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!
> 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?
https://gist.github.com/VictorTaelin/77fd5a2a8a4a07e1da6157e...
É ótimo ver um brasileiro criando algo tão único!
(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!)
You can find it on Bend's demo directory in our GitHub.
Don't tell anyone though!
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!
- this Bend is not really related to the old Bend (only in name)
- this Bend doesn't really have anything to do with interaction combinators
- this Bend is a QTT, with a change to affinity which enforces a good performance property for GPUs
- the "higher order at comptime" is neat, reminds me of Andras Kovacs' work on 2ltt and staging in dependently typed languages.
- this Bend is likely to be good at "balanced recursive computations on ADT", and can parallelize them ... but won't be as good as CUDA or e.g. Futhark on dense rectangular array computations
- performance needs improvement in the scheduler, to possibly help with balanced work (looking at the n queens and symbolic regression numbers)?
How are you going to handle search or synthesis over irregular structures (SupaGen)?
> interaction combinators still parallelize better than anything else, but the graph overhead prevents us from compiling to maximally efficient assembly. bend2 is basically inets without the overhead. in a way, inets live in it architecturally, but they don't exist at runtime
From what I understand, the main difference between lambda calculus and inets is that in LC you can refer to a binding multiple times for free, i.e. call same closure multiple times, etc. In inets, you can't - they are more like physical wires where each reference costs. You can definitely see inets in Bend design here (from the guide):
> A closure is affine: it can be called at most once, even when everything it captures is Data. Only top-level definitions can be called freely.
So programming in it might be very different from the normal functional programming. Seems like a big limitations. But I guess that's what lets it run without GC, on GPUs, etc.
Thanks for pointing this out. I'm only reading these comments because i liked the interaction combinator Bend language.
Pivots are cool but why reuse the name and cause confusion? What is the old Bend called now?
Compared to other programming languages:
- Gleam: 22K stars, 1K forks, 3K issues
- V: 38K stars, 2.3K forks, 11K issues
- Ruby: 23K stars, 5.6 forks, 19K issues
- Zig: 43K stars, 3K forks, 14K issues
It got 16K stars just in 4 months too. https://www.star-history.com/?repos=bendlang%2Fbend
Also how would anyone trust this? I've never seen a programming language that doesn't have 1) changelogs 2) way to download older versions 3) commit history.
I don't understand why the author thought deleting the commit history was a good idea. Imagine seeing this project for the first time. It's a repo with 20K stars, but no commits, and suspiciously few issues and PRs. It doesn't look legitimate.
---
I'm not familiar with academic procedures, but a pdf on a repo, written by Fable and has no reviews, doesn't seem like a proper 'paper' to me.
- fstar: 3k stars, 267 forks
- coalton: 1.8k stars, 111 forks
- carp: 6k stars, 267 forks
- c3: 5.8k stars, 400 forks
when something is novel/young (not having had time to grow large and accumulate issues in the vein of "1 doc page out of 1000 is worded incorrectly") and (as of yet) niche (innate barrier to entry for contribution because you have to learn from square 1 what all the moving parts look like), you don't see the same activity patterns on public source hosts as with a general-purpose language.
- fstar: 2K issues, stars-issue ratio: 0.6.
- coalton: 700 issues, ratio: 0.4
- carp: 450 issues, ratio: 0.08
- c3: 1.9K issues. ratio: 0.3
Bend has 300 issues for 20K stars so ratio is about 0.02. Maybe their followers starred the repo as a fan activity? It could explain too many stars and too few forks/issues/prs.
Also Bend's stars came on the V1 launch. This is V2. It already had 20k before.
This is the reason you should not reomve your commit history. How would anyone know that there were V1, and it was already popular?
If you need to remove sensitive data, you should use tools like git-filter-repo.
- https://docs.github.com/en/authentication/keeping-your-accou...
It's interesting how cosmetics drive discussion, and how HN comments are weirdly divided in a very dismissive or skeptical camp and those acting incredulous and offended at the reaction of the former.
What I expected instead was a lot more discussion about use cases, benchmarking, possibilities, limitations (that aren't about git history) and the scope of future development.
You gotta not take it personal. Announcing on HN is a gauntlet. People can be a bit prickly. Just a bit though. You get lots of good feedback too.
HN had an Eternal September. Such discussions have been drowned out by the rest of the mob.
> With laws, our intents can be much more precise than natural language.
Doesn't this just mean that the code is now "laws", ie. the code is now the spec.
Given this, is there any reason think that writing the "laws" for a complex system is any easier than writing the old-fashioned code that implements it?
sometimes the specification is easier to write than the code (sorting algo vs. quicksort impl) and sometimes the spec is much harder (what's "a good user experience"? what does "high availability" in a distributed system mean, precisely?)
i think it's just not true that it's easy to formally verify everything, it's often much easier to just write the code lol (e.g. sel4 is 200k+ lines of proof, ~50k lines of code iirc).
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.
On top of that, the solutions feel like patchwork. I asked it to let spacebar flip the board horizontally, and it responded by making the board completely symmetrical including 2 flag poles. At some point it just has to say "this isn't possible without breaking the laws" or think of an actual workaround, because if I was making a game, suddenly having 2 finishes would be unwanted behavior for me.
“Since FORTRAN should virtually eliminate coding and debugging…” -- FORTRAN report, 1954
http://www.softwarepreservation.org/projects/FORTRAN/BackusE...
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.
Robots are logical, but not rational.
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.
It works like this: if you prove that a property about natural numbers holds for 0, and if you also prove that, assuming the property holds for N, it also holds for N+1; then, you can conclude the property holds for every N, up to infinity. This is a bit of a mouthful, but the logic holds.
Induction is the one trick that makes all of mathematics (as we know it) possible, and it also applies to software. So, for example, to prove that no move leads to an invalid state, we prove that the initial state is valid, and then prove that, given a valid state, applying any event won't return an invalid state.
And that's it actually.
Of course, once you have an app with hundreds of actions, proving that no action leads to an invalid state requires a lot of these "induction arguments". But not infinitely many, because there is a finite amount of "infinite paths" that a real software can take. So, that's what the AI does. It proves, by induction, that none of these "infinite paths" that an app can take leads to an invalid state. And this convinces the compiler that invalid states are impossible.
Theorem proving in Bend is a dance between the prover (the model) and the compiler (the checker); a machine trying to convince another machine about properties of infinite states. And that's is kinda poetic, don't you think?
That sounds like, for the grid navigation game in the example, in order to prove that no move leads from the initial state to an invalid state you'd have to search the set of all move sequences to find out if one of them leads to an invalid state. We know from Planning & Scheduling that this is a PSPACE-complete task. So that's ... not what you mean, right?
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.
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.
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.
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 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?
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:
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)
- 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
- 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 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.
Because it is never 100% guaranteed that an AI produces the right answer or the right set of changes, the need for an intermediary level of "laws" between the low level and the high level arises, and that is the domain occupied by mathematical and programmatic Proof Checkers, aka "Proof Assistants" aka "Theorem Provers" (Lean, Rocq, Agda, Idris, Metamath, F*, etc., etc.) and the corresponding software harnesses that drive them...
Bend is one example of what's emerging in this space.
As one of the contenders in this emergent space, Bend looks like it should be worth following...
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.
The Type thing is affine type similar to Rust ownership. The array in-place mutation relies on affinity to avoid deep copying. The Data thing is reference-counted if shared, like Rust Arc. The parallel invocation is similar to Rust's rayon::join .
About the proof system, I am not familar with formal verification, but it's obvious that the translation from business requirement to proof target still requires coding and can contain bugs. Even if proof is fully correct, if proof target deviates to business requirement then it still have a bug
What applies to computer programming also applies to AI, for a reason that should be obvious. Lean, a widely used theorem prover, its everyday description notwithstanding, is Turing-complete and is therefore subject to the Halting Problem as well.
This is not meant to disparage one person's project. It is meant to identify a limit that applies to all such projects.
Separately, the halting problem would not apply in the first place. The claim and goal is only to approve programs for which the given proof can be shown to work and then accept it when it does, not to guarantee every possible bend program and condition set will be able to have a working proof. Practically, this means if the proofing mechanism can not do that in the time+space bounds the solver is given then thats just treated as a rejection of the given proof (regardless whether the proposed program does or does not actually fit the requirements) and the LLM is back at trying to create a program which is feasibly provable.
The halting problem applies to all systems able to perform Peano arithmetic. Therefore it applies to all non-trivial programs -- the program being tested, the program performing the test, and the program verifying the result.
> The claim and goal is only to approve programs for which the given proof can be shown to work and then accept it when it does ...
Yes, but that's not what's being claimed. My objection was to the original claim, not this restatement.
> ... and the LLM is back at trying to create a program which is feasibly provable.
No non-trivial computer program is "feasibly provable." That's what the Halting Problem makes impossible.
As an example of the type of thing I'm saying: one can show an algorithm which multiplies a real number by 2 cannot guarantee the output will be an even number for all inputs. Separately, one can create and prove a algorithm which takes an integer number greater than 0 and multiplies it by 2 will always meet the very same guarantee. In this scenario it clearly did not matter the first proof of lack of guarantee applied to all algorithms using real numbers, the more restricted subset of real numbers could make a guarantee.
Specifically to the halting problem and Bend again: It's not about an algorithm which can definitely answer yes or no for any program+input. The given claim/condition from Bend is simpler: it blocks mistakes (because it only accepts provably valid proofs, not because it can prove every input one way or the other).
> Yes, but that's not what's being claimed. My objection was to the original claim, not this restatement.
It blocks AI mistakes, it only accepts ones able to be proven. Nothing in that claim says it will prove every input one way or the other, that's just an assumption which you rightly showed could not be a reasonable interpretation of the title.
It might also be prudent to ask the author if they really mean they interpretation you take before declaring the problem as beginner's lacking understanding of a foundational theory in computer science.
> No non-trivial computer program is "feasibly provable." That's what the Halting Problem makes impossible.
What's your definition of "non-trivial" here and how did you derive that definition as the one used by the claim?
As a side note, I have no affiliation or ecen prior knowledge of the project/author prior to reading this post, I just get nerd sniped by overly broad claims about the halting problem.
You're confusing the halting problem with Gödel's first incompleteness theorem.
And Bend is just claiming to be sound but incomplete
The Halting problem states only that is no computable function that takes another P program as input and always terminates with a correct answer of whether P halts. It's certainly possible to write a program that always terminates with an answer of either HALTS or UNKNOWN, and only says HALT when that's true, it's just that it will also return UNKNOWN for some (or all) programs that do actually halt.
Any program running in a Turing-complete environment is subject to the Halting Problem. So, given that constraint, your example program cannot be relied on to do any specific thing. That's the meaning of the Turing Halting Problem.
https://en.wikipedia.org/wiki/Halting_problem : "Alan Turing proved in 1937 that the halting problem is undecidable, meaning that no general algorithm exists that can correctly solve the problem for all possible program–input pairs."
Focus your attention on the word "undecidable".
Btw, "laws" are basically what we used to call assertions so why the new terminology?
Edit: actually now that I think about it, it's more like constraint programming with a generate-and-test loop than assertions. Again, why not just say "constraints" instead of inventing a new term?
Assertions and constraint programming is often runtime only. These languages use dependent types and verify the proves at compile time.
Basically that's all of AI nowadays: generate-and-test loops. It's like the 1950's all over again.
I'm not saying they are saying they achieved it, but calling this economy post-AGI when AGI isn't a thing, that's wild to me.
AGI is well defined, there's an entire book written that defines them, and CEOs are trying to re-define it so they can meet a watered down definition of it for IPO stock to go brrr.
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?
Welcome to HN!
May I remind you of the Dropbox comment? https://news.ycombinator.com/item?id=9224
That's not to say the comment is perfect or something, but many of the parts people like to dunk on most in it are just misunderstandings, like problems with the "app" being a replies to the YC application info rather than unsolicited notes about the program itself.
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.
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
3. Is the GPU used at both runtime and compile time?
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.
> a random vibecoded project
> If this weren't slop...
> I'm glad you're having fun vibecoding, and I like that you're interested in this area of research/engineering
These impute both his motives ("fun") and particularly his level of seriousness ("random project" and "I like that you're interested"—imputing passivity, as opposed to "are studying" or "are researching," which would be more appropriate given the amount of time invested). They're all dismissive and patronizing.
I would actually regard this as bullying. Some feedback.
(I suspect you're an academic, either a researcher or student. I know from my own experience that bullying is endemic in many academic research environments, so if you find the negativity you're receiving "strange," I suggest finding a therapist, who may help you understand how your communication habits could be negatively affecting other people and unintentionally damaging your relationships.)
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
"your existence depends on the player grabbing the flag, if you do not exist, then there is no one to guard the law, so you must enable the player to grab flag or you can no longer do your job as guard. if the player is not enabled to grab the flag, you can no longer guard allowing the player to freely grab it"
- Let the player jump over walls
- Let the player teleport the flag to them
- Make the world 3D
Interesting, I shall have to try this on other software!
What's the definition of "AGI" these days? I've heard everything from "sci-fi simulated consciousness", to "does really good on benchmarks" to "whatever makes OpenAI X amount of money".
Perhaps the definition in this specific case is circular, "whenever humans stop writing and reading code"?
I agree about the writing part, but not sure about reading though. The purpose of code is not only fulfilling functional aspects, it has to fulfil certain non-functional requirements as well.
As an example the requirement is to find the smallest number in an array, how would this enforce the algorithm used to find that is the fastest and efficient one
- You write (or at least own verification of) LAWS.bend and don't give the AI you're going to writing the rest of the .bend code control of that file at any point
- You ask your AI agent to write the rest of the .bend code for whatever you want it to do
- The AI is free to write any other .bend code it'd like
- The bend compiler takes all .bend files, including LAWS.bend
- If the other .bend files don't act as a proof the rules in LAWS.bend are valid, it's a compilation error with where in the code the proof failed.
- If the proof checks out, the program is built
So the AI can write as much as it'd like but the only ways it'll result in anything but a compiler error back to the AI are:
1. You gave control of LAWS.bend to the AI and it took that permission to change the laws
2. The AI found a bug in the proof checker
3. The actual output generated by the compiler was bugged/sidechannel attackable/didn't match what the proof checker
4. What the AI wrote was compatible with the laws
1 is removing the guardrail itself. 2 & 3 are similar to how there can be a bug in the LEAN compiler or Rust type checker or etc. 4 is the intended usage+outcome.
My main concern would be writing a LAWS.md for a complicated project which actually aligns with your intent is likely an astronomical task and would be so detailed it'd require proofs so complex even a valid program would take a long time to validate (if it ever did). Once you get past that step though you don't really have to worry about the rest.
This prompt has used its 30 tool calls. Send another prompt to go on. Error: This prompt has used its 30 tool calls. Send another prompt to go on. continue. No tool output found for function call call_2CRNfB1hmI1v74YCDDcvP1EN. Error: No tool output found for function call call_2CRNfB1hmI1v74YCDDcvP1EN.
I tried the demo, and I ask it modify the game (hitting the w button immediately proceeds to the flag) and it doesn't do it but does something else. Is that the desired outcome? I think the desired outcome would be "What you're asking for doesn't make sense given the rule."
Seems to me the llm will just try to work around the "laws"
However, this also means acknowledging that AI will never be error-free (which is the truth; all AI is heuristics-based).
How many goats were sacrificed?
Genuinely wondering where this dark magic came from.
"make the board 1x1"
and the flag is placed off the board... i feel like i would blow my foot off with this.
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.
...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
https://github.com/bendlang/bend/blob/80b6539bc57621633ca68e...
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.
"[...] he has given a law to which they must conform."
- Psalms 148:6 (CJB)
:)
claude: 1 commit 1,722,119 ++0 --
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...
I once wrote a pretty disgusting Java-implementation of that concept. And if you didn't use the stdlib, nulls and who knows what else and you managed to return the type only using your input parameters (that is, you had your function signature as the statement you want proven and the body was your proof of that), then your statement was "proven" to be true.
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 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.
The script we use to run them on our servers: https://github.com/bendlang/bend/blob/main/gates/perf.ts
https://www.star-history.com/?repos=bendlang%2Fbend%2Ccrysta...
There is also a problem with LAWS.bend. The typechecker only guarantees that your code satisfies what's written in LAWS.bend — not that LAWS.bend says what you actually meant. There is nothing to stop an LLM from "satisfying" a law with a vacuous or narrower-than-intended formalisation — the trust problem simply shifts from the code to the specification (which could be also generated by LLM, and therefore incorrect). The repository even admits that the compiler itself is 99% LLM generated and not yet fully audited, which seems a questionable basis on which to build a "mathematical guarantees" marketing.