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.
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.
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
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.
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.
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 evolution 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".
>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".
But that doesn't mean anything. "Similar to" is vague enough that it could include video game NPC dialogue.
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.
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.
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.
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.
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?
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 remember how negative were the comments in your last submission here. They were unnecessary and I never understood why. I hope you get better comments now.
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.
That sounds like it's dead? The entire point of HVM as I understand was to be an incredibly fast evaluator. If bend2 does not use what right to exist does HVM still have?
no, that's a good question. half of the point of HVM is to be an incredibly fast evaluator, in the "raw speed" sense. the other is to be an incredibly fast evaluator, in the "asymptotical" sense. in the first sense, Bend2 supersedes HVM. in the last sense, HVM is still king. on higher order computations that involve λ-calculus and the like, nothing beats the HVM. but I also realize most people aren't doing λ-calculations. so, Bend is made for the general public and lower-order programs, while HVM remains for the niche group of researchers and λ-calculus enthusiasts
HVM was too be a highly parallel extremely efficient language target. Bend has taken that place in their ecosystem. I don't think that's weird question were that leaves HVM.
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!
My read on this, after ingesting a good amount of content on the history, is:
- 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)?
Here's what Victor wrote about inets in Bend2 (on X):
> 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.
aww man. I remember following victor in college. I mean pivots gotta pivot, and this is probably a better one for business, but always thought the interaction combinator framework was cool
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.
GitHub stars have been botted to hell for a long time now. I don't know how the farms acquire so many accounts, last time I tried to register a GitHub account I had to jump through so many hoops. The platform needs an overhaul, starting with requiring a valid payment method for the social features.
victor's legit and people have been excited about his work for years; squashing the history was just a bit of an optics oopsie on his part. the star to fork ratio makes perfect sense for something like bend.
- 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.
About forks alone I get it, but look at their issues.
- 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.
The project got a lot of attention at launch, but it wasn't really ready to be used back then. There were too many limitations, like u24 numbers (yes), 2 GB memory limit, pervasive strictness (if-then-else executed both branches). It was just not practical.I think (hope) that explains a lot of it. But honestly there is also my own failure into making the language actually be used, rather than just a viral moment :( I hope it will be different this time!
When the original bend released in 2024 it was mega-hyped, but then interest died off fairly quickly, hence the stars + lack of issues. Now they're re-using the same repo to release the new version.
victor has courted a very llm-enjoyer audience and such people are famously prone to hype (which is kinda brutal in its own way cause the language itself is cool and i dont wanna make it sound like im taking away from that). but yeah, fan activity as you put it easily accounts for the missing order of magnitude, if you like.
I honestly had no idea people would be so upset about commit history. I just wanted to avoid leaking sensitive info, that's all. I'm running through the commits to ensure nothing personal leaks and I plan on putting the history back.
Also Bend's stars came on the V1 launch. This is V2. It already had 20k before.
Unfortunately there's so much dishonesty and manipulation happening on the internet as of late, I feel like we've all become a bit distrustful of anything at first glance. I wouldn't take it personally. Best of luck with your project.
Gotta say, having followed Taelin on this project since mid 2023, this was not the response I expected when this language first dropped.
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.
> 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.
HN had an Eternal September. Such discussions have been drowned out by the rest of the mob.
> 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.
> 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?
Yeah i think empirically you've hit the nail on the head (and there are some ties here to computability theory, e.g. Rice's thm).
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).
100% agree. It's crazy so many Ai articles are heralding the end of code while at the same time defining more complex ways to write code under a different name.
I suppose I could look it up but I wonder if people thought this of "high level" languages like C when it first came out. No more assembly. Or even assembly instead of machine code.
This is the age old problem with proving correctness. You can (sometimes) prove that two programs have identical behaviour. One of the programs can be slightly simpler in that it is only concerned with what the correct result of a given operation is, not how to get there. But this doesn't fundamentally change that the complete specification is almost as complicated as the program itself.
Exactly. You could simplify things by giving AI a limited set of laws, but then you'd risk that AI would make some mistake in the parts that you didn't cover.
So a failsafe set of laws would look very much like an actual program.
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.
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
My main experience with the demo on the site is that I asked it to add a simple feature which would not even necessarily let you win the game, and it would spend >100k tokens in a loop of "laws broken" until maybe adding it, maybe not. After burning half a million tokens just to add an extra line of walls so that teleporting 2 squares up wouldn't let me win, my API key got rate limited and broke the loop.
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.
I think the demo is this way simply because looking at the LLM find wacky ways of implementing features without breaking the law is fun and drives the point across. In practice I imagine you would write something like "If you don't see a clear way of implementing a feature without breaking the law, ask me for directions" in AGENTS.md
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.
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.
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.
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.
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?
>> 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.
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?
Not the parent, but that's not the only way to prove stuff, depending on the exact configuration.
A bit of a contrived example, but let's say that the user starts at (0,0) and that all the four directions' movement will step 2. Then we can prove that all four directions will keep both the x and y coordinates' parity.
Now we apply the former theorem to our start position and can then conclude that after any number of steps the user will be on even x y coordinates. Now if the flag is on an odd coordinate we have proven that there is no way to get there, without searching the whole space.
For a less contrived example, it is also possible to work backwards from the goal, etc. The hard part of formal verification in general is that the proofs are closely coupled to the program code itself, so a different representation of state may make proving it more or less difficult to prove. And also code changes can easily break proofs, as the core of these languages is basically normalizing every expression to the max and comparing them (at that point basically programs) for equality.
Oh yes, if you know what problem you're trying to solve you can come up with clever ways to solve it cheaply: a heuristic.
The trouble is when you want to do that in the general case, i.e. when you don't know the problem you're solving. Unfortunately we don't know how to come up with heuristics automatically.
... well ish. We have relaxations in Planning again, but that really doesn't seem to have anything to do with what bend is doing.
Well, apparently we do have a non-deterministic black box that is pretty good at coming up with a bunch of heuristics ideas, and we also have a deterministic process to validate those ideas!
That's why I think getting formal verification "right" with LLMs will be huge.
>> Well, apparently we do have a non-deterministic black box that is pretty good at coming up with a bunch of heuristics ideas, and we also have a deterministic process to validate those ideas!
Do we? When have LLMs come up with heuristics? I'm sure if you ask an LLM to tell you e.g. how to solve a maze it will print out the instructions for the follow-the-left-wall heuristic, but that's not "coming up" with a heuristic.
I fear though we are about to go into one of those unproductive conversations about the capabilities of LLMs to produce novel results which I think has now reached saturation point all over the internets.
Well, it doesn't have to be novel, does it? Most of the real life problems are probably related to an already solved issue, so intelligent (probabilistic) recall is fruitful, even if it's "unoriginal".
Yes, it does. There are tons of things that we don't know how to get e.g. robots to do in the physical world and it seems that animals have a library of heuristics that let them do them cheaply and accurately. We totally want to be able to learn those heuristics of search for them and find them somehow.
And that's why my point was that we don't know how to come up with heuristics: because we currently don't.
Edit: if you mean that we can probabilistic-recall all those heuristics, that's not right. Because such heuristics are tacit knowledge that is very difficult, maybe even impossible, to articulate with enough accuracy to reproduce in a computer. We certainly can't get LLMs to learn them from the web because the web doesn't have text that explains e.g. how to control your muscles to climb a tree.
I honesty don't quite know what you argue about. That LLMs are not AGI? Of course not!
But this is a thread about a formal verification language, and in this area "just throwing non-deterministic proofs at it until something sticks" works kinda well.
And you just sort of said that something getting "figured out" by a random process with selection can't be a heuristic, as it has to be "novel" (whatever that means). Well, then unfortunately we have to exclude animals from that list as well, because if you read it again, that's pretty much how evolution works.
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
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.
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.
"You only have 10 seconds to make a first impression"
Glad you were able to restore the commit history.
With all the lack of authority of a random software developer on the Internet (but feel free to check my post history), I see the GitHub repo and its commit history as important and answers a few questions.
How old is this project ? (If one commit, I have no time range, so I have no way to know how long it has been worked on .)
Is it regularly updated? (If one commit, I can't tell the pace of updates)
Is it just one person, or a few people, or a community? (If only one commit, cannot see how many other people are available to support the project.)
If a project has no issues (no user complaints), then it's probably not used by anyone -- throw a rock and you can get one person to complain about how you changed the scenery, one person to complain about it being loud, one person to complain about how you threw it unergonomicly, and one person to criticize your accuracy. :) If it has no issues then probably no users.
Does it have any merged PRs? Open PRs? (If no merged PRs then presumably you do not really accept them? No way to know for sure but it's a signal.)
Of course these metrics can be gamed. But if you literally have only one commit, no issues, no PRs, then it's like declaring your restaurant is open for business but all the lights are off, there are no patrons, waiters, cooks, and there is a single to-go box on the table with a small bell next to it. Or it's a museum with only one exhibit and no docents or guests. It's just incredibly odd to see no history for a project.
Hmmm, this is interesting, because one might think of Software as a series of lower-level "laws", that is, specified in terms of the lines of the source code itself in whatever programming language it was written in, and (more recently, in the AI coding era) a set of higher-level, specified in human language "laws" that a coding assistant AI must also take into consideration (in addition to the code itself) when working on the code.
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...
> 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.
> 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.
We used to write programs without a compiler. We'd write them 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, 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 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?
It needs a special language for both. 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.
I've done my share of formal verification (see my old blog in my profile) and of programming in Assembly, and obviously the former is far harder than the latter. People have only managed to formally prove the correctness of programs (end-to-end) under ~10 KLOC. 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.
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 actually correctly implements matrix multiply 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 proven correct 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). It would be better to hand these as statements of fact (determined by a type checker) to the verifier rather than asking the verifier to first prove them from byte code and then do the actual correctness proof.
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. It's like saying that someone can boil an ocean or move a mountain, but we must order them a taxi to get there.
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”?
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.
You may want to take a look at how Rust deals with this. In Rust, even if T: !Copy, you can take a reference to an array element. If a language can't manage this sort of reference, you may need a more restrictive mechanism, perhaps as a pair of swaps (but then you need a default value) or some mechanism using closures that get called on the element and are required to return it.
I roughly check it. The array looks like tree in type defintion, where indexing is O(log n), but the real implementation seem to be real array with O(1)
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
Beginners in computer science need to understand that there's no such thing as a computer programming method or discipline that "blocks AI mistakes via proof." This is not a position or opinion, it is a fundamental constraint called the "Halting Problem," originally identified by Alan Turing in 1936.
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.
Graybeards in computer science sometimes need to remember the halting problem only states you cannot make a general algorithm which answers the halting question for all possible program+input pairs. Importantly, it does not state it's impossible to make an algorithm which can check if the given program+possible inputs will halt (or even if a given subset of all possible programs will - e.g., trivially, finitely long ones not given a means of recursion or allowed infinitely long inputs).
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.
> Separately, the halting problem would not apply in the first place.
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.
The halting problem applying to all systems is not the same as the halting problem being relevant to all claims about halting of systems (unless those claims can also be rigorously proven to match the conditions of the generalized halting problem first). I.e. I'm not trying to say the halting problem does not apply to these systems in general, I'm saying it doesn't apply to the specific claims being made about these systems.
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.
> It blocks AI mistakes, it only accepts ones able to be proven.
This is a simple restatement of the original claim, and it is false. The program being discussed is subject to the Turing Halting Problem. The program being tested, the same. Lean, the prover and the final authority, the same. All are subject to this fundamental limitation.
> It might also be prudent to ask the author if they really mean they interpretation you take
How the original author chose to express himself is not my problem, it is his. I have the simple responsibility to take him at his word. Anything else would be disrespectful.
> What's your definition of "non-trivial" here and how did you derive that definition as the one used by the claim?
I didn't define it, Alan Turing did, in 1936. It's not a debating point, it's a fundamental limitation. All Turing-complete code sources have this limitation. Read more here: https://en.wikipedia.org/wiki/Halting_problem .
> This is a simple restatement of the original claim, and it is false. The program being discussed is subject to the Turing Halting Problem. The program being tested, the same. Lean, the prover and the final authority, the same. All are subject to this fundamental limitation.
I disagree, which is why I added all of the additional commentary you appear to have ignored to restate your original claim instead. I'm not sure why I should restate my response to these points when they're still available and awaiting response above.
> How the original author chose to express himself is not my problem, it is his. I have the simple responsibility to take him at his word. Anything else would be disrespectful.
When someone's words on a project as complicated as this seems to violate the basic foundations of computer science it's both your problem & disrespectful to claim you know for certain the problem is because it's a common beginners mistake. This may be something we cannot come to an agreement on morally, but I suppose it won't really matter for the rest of the mathematical conversation which continues below.
> I didn't define it, Alan Turing did, in 1936. It's not a debating point, it's a fundamental limitation. All Turing-complete code sources have this limitation. Read more here: https://en.wikipedia.org/wiki/Halting_problem .
Wikipedia is a poor source to cite, but when I follow it I see no claim or definition by Turing for what non-trivial is. I see claim of what Rice meant by non-trivial in their eponymous theorem in 1951, but that's neither from 1936 nor a relevant definition for the current discussion so I must assume you mean somewhere else in Turing's actual paper I'd need to check.
Which takes us to the actual 1936 paper rather than Wikipedia's summary https://www.cs.virginia.edu/~robins/Turing_Paper_1936.pdf. I see 3 mentions of triviality, none of which appear to give a definition of what a non-trivial provably haltable example is:
1. Discussion of the remainder of the theorem itself being trivial [on page 31 of his paper, page 260 of the journal]
2. Since CC_0 is already been shown provable the conditional proof of the A(M)->CC_0 is trivial by the rules of implication [p32, 261 of the journal]
3. A trivial replacement of the variable naming scheme allows translation between the two notations without changing the calculus of them. [p34, 263 of the journal]
None of these seem to define what a non-trivially provable program (Turing Machine/Algorithm) is in context of the halting problem, so I again ask can you tell me where and what actual definition in Turing's actual 1936 paper you are using to define what a non-trivial program is so that I may apply this definition to the current conversation?
As another aside, one of my favorite "simplest" examples of a non-trivially provable program we know never halts despite the general case result of the halting problem:
for every group of positive integers (a,b,c,n) with n > 2:
if a^n + b^n = c^n:
halt
To prove this never halts you have to prove Fermat's last theorem. Which we have, and so we know this must never halt as you iterate infinitely over the positive integers, but it took one of the most complicated mathematical proofs known to show it.
There are certainly definitions of non-trivial where this is still considered trivial, but I'm at a loss to what part of Turing's paper gives such a definition.
>> This is a simple restatement of the original claim, and it is false. The program being discussed is subject to the Turing Halting Problem. The program being tested, the same. Lean, the prover and the final authority, the same. All are subject to this fundamental limitation.
> I disagree ...
This is not a topic open to debate, it is a statement of fact. I strongly recommend that you learn this topic, and the topics of mathematics and logic, where some statements can be proven true or false without ambiguity.
The Turing Halting Problem applies to all Turing-complete environments. The program under discussion meets the criterion. AI meets the criterion. Lean meets the criterion.
> There are certainly definitions of non-trivial ...
If you wish to say you have a counterclaim to the idea mistakes can be blocked regardless if every program can be proven to halt which is based in mathematical reasoning you must be able to state or produce the claim in the actual mathematical reasoning itself (or at least a link to the specific math directly relevant to the claim), not an English text summary of an entire paper/problem on Wikipedia. Anything less is not mathematical reasoning.
I'm unable to say more at this point as I can only assume you will continue to use that as a chance to quote and discuss everything but actual mathematics.
> If you wish to say you have a counterclaim to the idea mistakes can be blocked regardless if every program can be proven to halt which is based in mathematical reasoning you must be able to state or produce the claim in the actual mathematical reasoning itself ...
This is not a philosophy discussion, and Alan Turing already plowed this ground. The original claim "Bend - a language that blocks AI mistakes via proof [...]" is unsupportable.
> ... if every program can be proven to halt ...
But that's not so. You have introduced a qualifier that is known to be false.
> ... a chance to quote and discuss everything but actual mathematics.
Yes, I agree -- you should stop doing that. I keep referring to the original technical reason the original claim is unsupportable, others keep raising objections without trying to think through their positions.
It's not as though the Halting Problem is on the Millennium Prize Problem list, open to contradiction/reconsideration by some future challenge. It's a theorem, not a conjecture.
I've given notes of where in Turing's paper any type use triviality could be found, with direct page citations of the relevant original math, along with the mathematical reasons it doesn't have anything to do with the plain English statements you are making. This effort was a kindness done in good faith that I might find said mathematical definition of non-triviality for the halting problem somewhere in the paper, not something needed to show your claim devoid of a shown basis in mathematical reasoning so far. That much is apparent by the lack of a single mathematically defined claim specified by any of your messages.
That said, if you'd like me to formally show what e.g. the triviality in the rules of implication Turing was talking about are in a purely mathematical form I'd be glad to state with no English commentary out of good faith as well. This would seem a waste of time unless that's the part of the paper you think the definition of non-triviality can be sourced, but at least I'd at last have a clear mathematical claim from you to discuss.
It is now your opportunity to make a mathematical claim, of which proof by assertion this paper should apply because it proves something in general is not.
> That much is apparent by the lack of a single mathematically defined claim specified by any of your messages.
I posted the Turing Halting Problem Wikipedia page. It describes a theorem, not a conjecture that I need to prove, which shows the original poster's claim is contradicted by established facts.
Let me put it this way. If I say, "There are an infinity of primes," will you reply, saying, "I disagree"? That position would be equally appropriate -- that is to say, not appropriate at all.
Am I obliged to prove the infinity of primes by generating an infinity of candidate integers and prove that some of them are prime? No, and by the same token, I'm not obliged to reply to your naive demands and teach you why the Halting Problem falsifies the claim made by the original poster. That is not my responsibility, it is yours.
In mathematics, some things are conjectures -- the Millennium Challenge problems, for example. Others are theorems, meaning established truths, beyond dispute. Turing's Halting problem is a theorem.
The question in the title is rhetorical, as you will discover if you read and understand the article I just linked.
> It is now your opportunity to make a mathematical claim, of which proof by assertion this paper should apply because it proves something in general is not.
How many more mathematical literature references will you require before you realize I have already met any burden of proof? I could post the entire technical proof here, but (a) the editors of this forum would kick me out, and (b) you would still refuse to accept the evidence.
How do I know this? Because you keep refusing to learn what you need to know to engage in this conversation.
The answer to what I'd say if this were about primes and a program which blocks outputting them in pure mathematics, despite there being infinitely many, would be (using a similar type of argument I gave early on for the current discussion):
(Apologies for the formatting, HN does not allow latex)
The thing blocking me from being able to do the same here is I defined a similarly styled argument about it being possible to construct a program (glad to give it in pure math if tou'd like) which blocks all non-halting programs by only allowing ones showable to be halting (n.b. much as the above example with primes, this result did not require listing every non-halting program and so does not disagree with the general halting problem) and you said Turing's paper contains some definition of non-triviality which says why that cannot be and then refuse to say what and where in this paper you believe this definition of non-triviality to be even though I could find no such thing.
If you said Euclid showed the above proof on primes does not apply because he gave some definition of non-triviality, telling me it's somewhere in his book Elements, and I said book IX proposition 20 does not say anything like that, so you say "it's on Wikipedia"... you could see why I have doubts you have any mathematical claim to produce defining said definition. At the very least, you could see how I'd still be awaiting to hear the actual mathematics you're using.
> The answer to what I'd say if this were about primes and a program which blocks outputting them in pure mathematics, despite there being infinitely many, would be ... [ snip ] ... Q.E.D.
Now I get it. I should have realized at the outset that this outcome lay in the future. You are here to pointlessly argue, not discuss nor debate.
> At the very least, you could see how I'd still be awaiting to hear the actual mathematics you're using.
Yes -- notwithstanding that I have posted links to that exact evidence from multiple sources. The problem is not a lack of evidence, the problem is that you refuse to read it.
Andrew Wiles conclusively (dis)proved Fermat's Last Theorem. If you disagree, and since you have demonstrated a willingness to disagree with anything, I would have to post a link to the evidence, not the evidence itself, because the (dis)proof is 129 pages long.
As I post this, I'm trying to imagine the corpus of mathematical knowledge you're unwilling to accept, because it won't fit into a finite-sized Hacker News post -- relativity, both special and general, quantum mechanics, dozens of others.
I'm also trying to imagine someone whose literacy filter consists of "Tl;DR!"
It truly breaks my heart to see any of the math snipped out yet again. You sound more than capable of formulating your assertions in pure math but seemingly refuse to state it that way, which feels like watching a bright light in the world going out as it seeks to avoid rigor.
A set of theorems (of which I accept all you've named) without the definitions of exactly how and why they apply to the give problem is no more mathematics than a bunch of bricks is a chimney. I believe all of these beautiful proofs, I just don't believe you've properly demonstrated you can build your chimney with them. If you ever wish to build the chimney I'd be ecstatic, until then I think I don't think anything else can be said about how the pile of bricks aren't an example of one - especially if you're going to give the URL I already provided you when asking where the definition of the connection in it was https://news.ycombinator.com/item?id=49761146
I do wish you well and I'm sorry if my requirement for rigorous statements in math seems pointless to you. It's something I hold dear. I'll keep notifications in my script enabled in case you do want to start discussing the math rigorously, but I'll no longer try to convince you that's what's needed for your claims to hold mathematical weight anymore or any of the other things which seem to be bothering you for no gains.
> A set of theorems (of which I accept all you've named) without the definitions of exactly how and why they apply to the give problem is no more mathematics than a bunch of bricks is a chimney.
A second reply. What you're not getting is that the mathematical equations in Turing's paper don't make its point. There are plenty of equations, but the paper's meaning lies in its logical arguments, for which the equations can only play a supporting role.
If the equations are taken out of the paper and presented separately, as you have repeatedly demanded, the paper's thesis falls apart. But to understand this, you would have to read the paper itself and absorb Turing's logical arguments. And the paper can't be made shorter without losing its meaning.
More evidence for this is given by the fact that Alonzo Church published a similar paper in 1936, different author, different equations, but the same logical argument and conclusion, such that Church and Turing are now given equal credit for the basic idea -- an idea that is supported by equations but not provided by them (https://courses.fit.cvut.cz/MI-VYC/church-a-note-on-the-ents...).
This is true in many parts of mathematics and logic. Another example is Einstein's 1905 paper later identified as the source of "special relativity". If you remove the equations and present them separately, all meaning is lost. In fact, in that case, the actual meaning of a particular equation was lost to Einstein himself, but that meaning occurred to his former math teacher Hermann Minkoswski, who went on to publish about something Minkowski called "spacetime". As before, the equations didn't convey the paper's real meaning, they could only play a supporting role. About this outcome Einstein later said, "Since the mathematicians have invaded relativity theory, I don't understand it myself any more."
Another more recent example is the recently solved "Navier–Stokes existence and smoothness problem" as it was titled by the Clay Mathematics Institute. The equation is easy to render, but as with the other examples, the problem to be solved goes far beyond the equation itself, and the meaning of the recent result lies not in the equation, but in its treatment and processing by AI.
In Navier-Stokes, everyone had access to the equations, but until recently no one could answer a fundamental question about it, and as with the prior examples, the real meaning requires one to read the articles that provide the logical reasoning. In each of these examples and many more, listing the equations can only be a preliminary step to true understanding.
More importantly, the meaning of the papers cannot be summarized in fewer words than are provided by the papers themselves. Mathematicians don't go out of their way to make their papers longer than their contents require, in fact, quite the opposite.
I can't believe you're still expecting bumperstickers to stand in for technical articles. As before, you should read the original articles instead of complaining that they're too long for your limited attention span.
> There are plenty of equations, but the paper's meaning lies in its logical arguments
This is the difference I feared. I trust, understand, and take lead of the rigorous math of the paper, you opt to follow in English arguments of what you think it's supposed to mean or apply to. No matter how much math is discussed, it'll never lead to anything if that's not where your understanding of the paper comes from.
It's one of the main things which separate hard sciences from things like Psychology where anyone can just talk about what they understand/see or want to link instead of define it in logic itself, and I must admit I've never believed much of the soft sciences because of that lack of rigor. Maybe that rejection of soft science as truth is a limitation of mine :) but I don't see myself abandoning the view any time soon.
> It truly breaks my heart to see any of the math snipped out yet again.
A false statement. I posted a link to the evidence, which cannot be summarized to satisfy your short attention span. Your unwillingness to read it only reveals your shallow grasp of modern technical topics.
Here is a short list of topics that cannot be converted into bumperstickers, your preferred medium of expression:
Special and General Relativity
Quantum Physics et. al.
Cosmology
Biology
Modern Set Theory
This list is by no means complete, but the last entry overlaps with the topic of this conversation, for reasons that will not be obvious to you unless and until you overcome your distaste for evidence.
> I do wish you well and I'm sorry if my requirement for rigorous statements in math seems pointless to you.
Excuse, me, what? I have posted links to the evidence that proves your position to be false, but you won't read it. You are to modern times what a religious fundamentalist is to science -- the primary obstacle to human progress.
Am I saying your unwillingness to absorb ideas outside your short attention span is itself an obstacle to human progress? No, actually, I'm saying you should avoid drawing conclusions without first examining the evidence.
It isn't only that you won't read the evidence that proves your position to be wrong -- that is simply sad, not fatal. It is that you draw conclusions without first examining the readily available evidence.
> A set of theorems (of which I accept all you've named) without the definitions of exactly how and why they apply to the give problem is no more mathematics than a bunch of bricks is a chimney.
Wow. You just dismissed the validity of all the topics in my list above, each of which produce everyday valid conclusions derived from very complex logical and mathematical antecedents.
You are the one being insufficiently precise here. There would only be fundamental obstacles if there was an additional claim "allows all correct programs".
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.
> 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."
I like it. It's like Bogosort- the Language. It would work much better if a) tokens were free and b) computation, therefore retries, didn't take any time at all. In the current world it's going to be fun watching LLMs getting stuck in infinite loops, doing and undoing their work to try and uphold a law they don't know how to uphold.
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?
“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.
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.
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.
Giving it a paradox yields interesting results. I'm not sure what its proving other than there will be cases that proofs can't help you with. I can't think of a practical example.
"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"
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
3. Is the GPU used at both runtime and compile time?
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.
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?
> 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.)
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. 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.
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
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"?
> In the post-AGI economy, humans will eventually 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.
Well, didn't win, but definitely broke it. Needs an edge case handler for tool call exhaustion:
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'm interested in how to integrate formal verification with existing software libraries. For example, https://github.com/verus-lang/verus integrates proof with macro in Rust. What's the plan for Bend?
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."
Yeah, but this assumes the llm will follow the "Laws". I find llms routinely ignore steering docs etc, even outright instructions. Like "Dont use python", next line it is trying to use Python.
Seems to me the llm will just try to work around the "laws"
No, it doesn't assume that. It simply assumes that you can verify whether or not the LLM's implementation adheres to the laws you defined up-front — which it does not if it modified the laws.
Exactly, you can have all the laws, but an LLM (or even a human) will just delete or refine the laws and hide the change in a 5kloc PR, that the "code author" will not review carefully, and you have 5 min to review and stamp to make sure your company is moving fast...
If the LLM changes the laws to bypass them that's on you. The whole point of this is that you don't have to manually review most code written; only the laws. If the LLM changes the laws and you ignore it that's a you problem.
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.
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%.
...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?
To give you a concrete reason why you should care to preserve the exact history and why it’s a matter of trust: in your paper, you reported the pinned SHA head of the benchmarks you ran. 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?
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.
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?
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.
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.
Well, yeah. Most are just unsound and not too useful (e.g. can only state propositional logic statements).
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.
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.
Have we delegated writing code to "AGIs" so we can write code to proof that the slop code works?
I have a vague memory of pre-AGI era, when we wrote things called "tests" to verify that our code did what it claimed to do.
20k stars is about the same as Crystal and Gleam, languages with actual user bases that have been around for years. Here’s what organic versus… we’ll say viral growth looks like.
As I understand it, there are no implicit arguments (and, consequently, no unification) here, right? This doesn't seem very serious given the ambitions of a project like this. Of course, one could argue that it isn't necessary if everything is generated by a LLMs, but… why bother with "human-readable" Python-like syntax in that case? It's not Python, after all, and I don't think it would help with LLM code generation in any way.
And benchmarking this language against Isabelle/Agda/Lean/Rocq is strange. The time taken for those systems to perform their checks is mostly spent on elaboration, which includes unification against metavariables, typeclass resolution and tactics. Bend has none of that (there are no type classes or traits, and according to the README, everything must be fully annotated and nothing inferred). This means that the benchmark is comparing Bend's checker to the other systems' elaborators + kernels rather than their kernels (Agda doesn't have this separation though). The latter would be a fairer comparison, and in this area the other systems are already fast. Framing it as "outperforming every proof assistant" without that caveat is misleading.
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.
Hi, I'm the author.
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!
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.
> LAW: "the sum of all balances in this contract must be zero"
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.
Gross, obvious exploits can be easily picked up by AI reviews.
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.
And then the agentic loop over the reviews will rewrite them into less obvious exploits.
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
Discover the laws in a current code base?
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.
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.
I don’t think that’s right.
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.
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.
you might be interested in property-based testing, which somewhat enumerates tests based on invariance and induction
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.
Natural language is ambiguous. Specifying exactly what you want in a way that is truly verifiable is the act of coding.
Start printing the t-shirts!
You mean t-shirts of this comic, from 2016?
[0] https://www.commitstrip.com/en/2016/08/25/a-very-comprehensi...
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.
The computer from Star Trek sounds like it could entirely plausibly have been made with LLM components and a century of harness tweaking piled on.
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 evolution from Kermit the Frog.
It's a thing you can talk to that does stuff for you. What other "architecture" do you need to know?
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."
Literally not what the comment you were replying to was saying even remotely, but ok.
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".
>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".
But that doesn't mean anything. "Similar to" is vague enough that it could include video game NPC dialogue.
Bend would make Dijkstra happy even when proof checking can’t verify if the laws are what was actually meant.
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.
[dead]
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.
> writing the laws becomes a bigger problem than writing the code itself.
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.
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.
> writing the laws becomes a bigger problem than writing the code itself.
Of course because at its limit programming is basically defining desired behaviour under all circumstances and logical conditions.
Heh, We're writing Asimov in real life after been warned to decades.
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.
Well described the problem scope.
I wonder if harness-hooks + Jev (equivalents) could semantically lint for `sloppy_law` etc when ever they are edited
[flagged]
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.
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.
I will improve that phrasing, thanks.
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!
Hi author :wave:
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.
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?
A lot of information here:
https://gist.github.com/VictorTaelin/77fd5a2a8a4a07e1da6157e...
https://github.com/victortaelin
[dead]
Congrats, Victor!
É ótimo ver um brasileiro criando algo tão único!
obrigado amg
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!)
Does Bend have linear types? I didn't see anything on them in a quick skim of the GUIDE file.
the entire language is based on linear types! it says so in the GUIDE yes
Ah, thanks, was looking at the readme instead of the guide
Thank you.
Maybe you can explain or give a hint, why a function that never returns could prove anything?
I remember how negative were the comments in your last submission here. They were unnecessary and I never understood why. I hope you get better comments now.
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.
what happened to your other project? HVM?
Surprise - HVM has been reimplemented in Bend 2.
You can find it on Bend's demo directory in our GitHub.
Don't tell anyone though!
i'm asking you what happened to HVM that it needed to be reimplemented as Bend.
It didn't "need to", it just evolves by rewrites as I learn (the project is fairly small) so in the latest rewrite I choose Bend!
That sounds like it's dead? The entire point of HVM as I understand was to be an incredibly fast evaluator. If bend2 does not use what right to exist does HVM still have?
no, that's a good question. half of the point of HVM is to be an incredibly fast evaluator, in the "raw speed" sense. the other is to be an incredibly fast evaluator, in the "asymptotical" sense. in the first sense, Bend2 supersedes HVM. in the last sense, HVM is still king. on higher order computations that involve λ-calculus and the like, nothing beats the HVM. but I also realize most people aren't doing λ-calculations. so, Bend is made for the general public and lower-order programs, while HVM remains for the niche group of researchers and λ-calculus enthusiasts
>If bend2 does not use what right to exist does HVM still have?
What? This is such a weird comment.
HVM was too be a highly parallel extremely efficient language target. Bend has taken that place in their ecosystem. I don't think that's weird question were that leaves HVM.
Thank you for adding a 5-line AGENTS.md. Other projects force you to install skills or MCP even when they're just doing the same thing.
Speaking of lava, you should do a presentation to the local tech group if you're ever here in Bend, Oregon...
This is a nice reminder for people.
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!
Glad to see this finally released! What are you doing next?
honestly just Bend is a great HN title, you can describe it more concretely on the homepage
Thank you for being honest.
[dead]
[dead]
[dead]
[flagged]
My read on this, after ingesting a good amount of content on the history, is:
- 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)?
Here's what Victor wrote about inets in Bend2 (on X):
> 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 clarifying. I would like to see a more clear exposition on the relationship here.
aww man. I remember following victor in college. I mean pivots gotta pivot, and this is probably a better one for business, but always thought the interaction combinator framework was cool
What?
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?
[dead]
This project's repo has 20K stars with only 500 forks, with less than 300 issues(including closed). Something's not right.
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.
GitHub stars have been botted to hell for a long time now. I don't know how the farms acquire so many accounts, last time I tried to register a GitHub account I had to jump through so many hoops. The platform needs an overhaul, starting with requiring a valid payment method for the social features.
victor's legit and people have been excited about his work for years; squashing the history was just a bit of an optics oopsie on his part. the star to fork ratio makes perfect sense for something like bend.
- 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.
About forks alone I get it, but look at their issues.
- 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.
The project got a lot of attention at launch, but it wasn't really ready to be used back then. There were too many limitations, like u24 numbers (yes), 2 GB memory limit, pervasive strictness (if-then-else executed both branches). It was just not practical.I think (hope) that explains a lot of it. But honestly there is also my own failure into making the language actually be used, rather than just a viral moment :( I hope it will be different this time!
commit history is back now!
When the original bend released in 2024 it was mega-hyped, but then interest died off fairly quickly, hence the stars + lack of issues. Now they're re-using the same repo to release the new version.
This obsession over GitHub stars is quite bizarre.
victor has courted a very llm-enjoyer audience and such people are famously prone to hype (which is kinda brutal in its own way cause the language itself is cool and i dont wanna make it sound like im taking away from that). but yeah, fan activity as you put it easily accounts for the missing order of magnitude, if you like.
I honestly had no idea people would be so upset about commit history. I just wanted to avoid leaking sensitive info, that's all. I'm running through the commits to ensure nothing personal leaks and I plan on putting the history back.
Also Bend's stars came on the V1 launch. This is V2. It already had 20k before.
> 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...
- https://github.com/newren/git-filter-repo
Commit history is back!
Unfortunately there's so much dishonesty and manipulation happening on the internet as of late, I feel like we've all become a bit distrustful of anything at first glance. I wouldn't take it personally. Best of luck with your project.
If you're distrustful of anything, why do you trust the number of git stars? It's something easily botted after all.
Who said that I do trust that?
Gotta say, having followed Taelin on this project since mid 2023, this was not the response I expected when this language first dropped.
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.
This is actually the typical case when new projects drop on HN. Dropbox is the canonical example.
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.
> 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.
HN had an Eternal September. Such discussions have been drowned out by the rest of the mob.
That crowd is moved to X these days, in my experience. HN became mostly the folks who didn't notice.
You can find everything on X, from dumpster fires to peak intellectual, everything in between.
Less so, here.
hn is just a bunch of wannabes these days. It's still a decent link aggregator but the discussions are exceptionally weak <shrug>
Every place I ever join is declared a shadow of its former self shortly after, it's like a curse.
so it's YOUR fault then, get em boys!
> 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.
> 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?
Yeah i think empirically you've hit the nail on the head (and there are some ties here to computability theory, e.g. Rice's thm).
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).
100% agree. It's crazy so many Ai articles are heralding the end of code while at the same time defining more complex ways to write code under a different name.
I suppose I could look it up but I wonder if people thought this of "high level" languages like C when it first came out. No more assembly. Or even assembly instead of machine code.
This is the age old problem with proving correctness. You can (sometimes) prove that two programs have identical behaviour. One of the programs can be slightly simpler in that it is only concerned with what the correct result of a given operation is, not how to get there. But this doesn't fundamentally change that the complete specification is almost as complicated as the program itself.
Exactly. You could simplify things by giving AI a limited set of laws, but then you'd risk that AI would make some mistake in the parts that you didn't cover. So a failsafe set of laws would look very much like an actual program.
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.
Problem is the stdlib is very small so proving even simple theorems still takes a lot more effort (for the AI) than in Lean. We need a mathlib!
> LAWS.bend
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.
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
My main experience with the demo on the site is that I asked it to add a simple feature which would not even necessarily let you win the game, and it would spend >100k tokens in a loop of "laws broken" until maybe adding it, maybe not. After burning half a million tokens just to add an extra line of walls so that teleporting 2 squares up wouldn't let me win, my API key got rate limited and broke the loop.
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.
I think the demo is this way simply because looking at the LLM find wacky ways of implementing features without breaking the law is fun and drives the point across. In practice I imagine you would write something like "If you don't see a clear way of implementing a feature without breaking the law, ask me for directions" in AGENTS.md
> humans will eventually stop writing and reading code,
“Since FORTRAN should virtually eliminate coding and debugging…” -- FORTRAN report, 1954
http://www.softwarepreservation.org/projects/FORTRAN/BackusE...
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.
[1] https://hdl.handle.net/10779/uos.32024301
The issue is I’ll have to vibecode all the laws and the laws could be wrong.
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.
I take it you haven't used Microsoft Windows?
Joking, joking...
That's an old "AI" joke. It went like that:
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.
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.
Indeed
Robots are logical, but not rational.
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.
LLM driven agents aren’t even that.
Words of wisdom.
true
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.
For Lean I understand how it works, here not.
You can prove infinitely many cases by induction.
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?
>> 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.
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?
Not the parent, but that's not the only way to prove stuff, depending on the exact configuration.
A bit of a contrived example, but let's say that the user starts at (0,0) and that all the four directions' movement will step 2. Then we can prove that all four directions will keep both the x and y coordinates' parity.
Now we apply the former theorem to our start position and can then conclude that after any number of steps the user will be on even x y coordinates. Now if the flag is on an odd coordinate we have proven that there is no way to get there, without searching the whole space.
For a less contrived example, it is also possible to work backwards from the goal, etc. The hard part of formal verification in general is that the proofs are closely coupled to the program code itself, so a different representation of state may make proving it more or less difficult to prove. And also code changes can easily break proofs, as the core of these languages is basically normalizing every expression to the max and comparing them (at that point basically programs) for equality.
Oh yes, if you know what problem you're trying to solve you can come up with clever ways to solve it cheaply: a heuristic.
The trouble is when you want to do that in the general case, i.e. when you don't know the problem you're solving. Unfortunately we don't know how to come up with heuristics automatically.
... well ish. We have relaxations in Planning again, but that really doesn't seem to have anything to do with what bend is doing.
Well, apparently we do have a non-deterministic black box that is pretty good at coming up with a bunch of heuristics ideas, and we also have a deterministic process to validate those ideas!
That's why I think getting formal verification "right" with LLMs will be huge.
>> Well, apparently we do have a non-deterministic black box that is pretty good at coming up with a bunch of heuristics ideas, and we also have a deterministic process to validate those ideas!
Do we? When have LLMs come up with heuristics? I'm sure if you ask an LLM to tell you e.g. how to solve a maze it will print out the instructions for the follow-the-left-wall heuristic, but that's not "coming up" with a heuristic.
I fear though we are about to go into one of those unproductive conversations about the capabilities of LLMs to produce novel results which I think has now reached saturation point all over the internets.
Well, it doesn't have to be novel, does it? Most of the real life problems are probably related to an already solved issue, so intelligent (probabilistic) recall is fruitful, even if it's "unoriginal".
Yes, it does. There are tons of things that we don't know how to get e.g. robots to do in the physical world and it seems that animals have a library of heuristics that let them do them cheaply and accurately. We totally want to be able to learn those heuristics of search for them and find them somehow.
And that's why my point was that we don't know how to come up with heuristics: because we currently don't.
Edit: if you mean that we can probabilistic-recall all those heuristics, that's not right. Because such heuristics are tacit knowledge that is very difficult, maybe even impossible, to articulate with enough accuracy to reproduce in a computer. We certainly can't get LLMs to learn them from the web because the web doesn't have text that explains e.g. how to control your muscles to climb a tree.
I honesty don't quite know what you argue about. That LLMs are not AGI? Of course not!
But this is a thread about a formal verification language, and in this area "just throwing non-deterministic proofs at it until something sticks" works kinda well.
And you just sort of said that something getting "figured out" by a random process with selection can't be a heuristic, as it has to be "novel" (whatever that means). Well, then unfortunately we have to exclude animals from that list as well, because if you read it again, that's pretty much how evolution works.
[dead]
If your game is big, then your proof will need to be huge. It works basically the same as Lean.
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 to code now, and the author wants his product to be used. I think it makes sense.
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
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.
should I read this as "I wish I could find a guy like you" :')
Congrats on the launch!
Question, does the parallelism work on M-Series GPU? The page says CUDA parallelism but shows Mac performance numbers.
Thank you!!
Currently, parallelism works in any multi-core CPU, and in Apple M-series and NVIDIA GPUs.
super cool! will try it out on some sci-sim work soon
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.
I'll try to sanitize the commit history, I had no idea it would be so important
Commit history is back!
"You only have 10 seconds to make a first impression"
Glad you were able to restore the commit history.
With all the lack of authority of a random software developer on the Internet (but feel free to check my post history), I see the GitHub repo and its commit history as important and answers a few questions.
How old is this project ? (If one commit, I have no time range, so I have no way to know how long it has been worked on .)
Is it regularly updated? (If one commit, I can't tell the pace of updates)
Is it just one person, or a few people, or a community? (If only one commit, cannot see how many other people are available to support the project.)
If a project has no issues (no user complaints), then it's probably not used by anyone -- throw a rock and you can get one person to complain about how you changed the scenery, one person to complain about it being loud, one person to complain about how you threw it unergonomicly, and one person to criticize your accuracy. :) If it has no issues then probably no users.
Does it have any merged PRs? Open PRs? (If no merged PRs then presumably you do not really accept them? No way to know for sure but it's a signal.)
Of course these metrics can be gamed. But if you literally have only one commit, no issues, no PRs, then it's like declaring your restaurant is open for business but all the lights are off, there are no patrons, waiters, cooks, and there is a single to-go box on the table with a small bell next to it. Or it's a museum with only one exhibit and no docents or guests. It's just incredibly odd to see no history for a project.
yeah that makes sense, thanks for the feedbacks!
Hmmm, this is interesting, because one might think of Software as a series of lower-level "laws", that is, specified in terms of the lines of the source code itself in whatever programming language it was written in, and (more recently, in the AI coding era) a set of higher-level, specified in human language "laws" that a coding assistant AI must also take into consideration (in addition to the code itself) when working on the code.
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...
> 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.
> 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.
We used to write programs without a compiler. We'd write them 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, 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 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?
It needs a special language for both. 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.
I've done my share of formal verification (see my old blog in my profile) and of programming in Assembly, and obviously the former is far harder than the latter. People have only managed to formally prove the correctness of programs (end-to-end) under ~10 KLOC. 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.
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 actually correctly implements matrix multiply 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 proven correct 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). It would be better to hand these as statements of fact (determined by a type checker) to the verifier rather than asking the verifier to first prove them from byte code and then do the actual correctness proof.
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. It's like saying that someone can boil an ocean or move a mountain, but we must order them a taxi to get there.
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:
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.
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).
Thanks for your questions and patience!
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”?
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.
You may want to take a look at how Rust deals with this. In Rust, even if T: !Copy, you can take a reference to an array element. If a language can't manage this sort of reference, you may need a more restrictive mechanism, perhaps as a pair of swaps (but then you need a default value) or some mechanism using closures that get called on the element and are required to return it.
I roughly check it. The array looks like tree in type defintion, where indexing is O(log n), but the real implementation seem to be real array with O(1)
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
Beginners in computer science need to understand that there's no such thing as a computer programming method or discipline that "blocks AI mistakes via proof." This is not a position or opinion, it is a fundamental constraint called the "Halting Problem," originally identified by Alan Turing in 1936.
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.
Graybeards in computer science sometimes need to remember the halting problem only states you cannot make a general algorithm which answers the halting question for all possible program+input pairs. Importantly, it does not state it's impossible to make an algorithm which can check if the given program+possible inputs will halt (or even if a given subset of all possible programs will - e.g., trivially, finitely long ones not given a means of recursion or allowed infinitely long inputs).
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.
> Separately, the halting problem would not apply in the first place.
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.
The halting problem applying to all systems is not the same as the halting problem being relevant to all claims about halting of systems (unless those claims can also be rigorously proven to match the conditions of the generalized halting problem first). I.e. I'm not trying to say the halting problem does not apply to these systems in general, I'm saying it doesn't apply to the specific claims being made about these systems.
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.
> It blocks AI mistakes, it only accepts ones able to be proven.
This is a simple restatement of the original claim, and it is false. The program being discussed is subject to the Turing Halting Problem. The program being tested, the same. Lean, the prover and the final authority, the same. All are subject to this fundamental limitation.
> It might also be prudent to ask the author if they really mean they interpretation you take
How the original author chose to express himself is not my problem, it is his. I have the simple responsibility to take him at his word. Anything else would be disrespectful.
> What's your definition of "non-trivial" here and how did you derive that definition as the one used by the claim?
I didn't define it, Alan Turing did, in 1936. It's not a debating point, it's a fundamental limitation. All Turing-complete code sources have this limitation. Read more here: https://en.wikipedia.org/wiki/Halting_problem .
> This is a simple restatement of the original claim, and it is false. The program being discussed is subject to the Turing Halting Problem. The program being tested, the same. Lean, the prover and the final authority, the same. All are subject to this fundamental limitation.
I disagree, which is why I added all of the additional commentary you appear to have ignored to restate your original claim instead. I'm not sure why I should restate my response to these points when they're still available and awaiting response above.
> How the original author chose to express himself is not my problem, it is his. I have the simple responsibility to take him at his word. Anything else would be disrespectful.
When someone's words on a project as complicated as this seems to violate the basic foundations of computer science it's both your problem & disrespectful to claim you know for certain the problem is because it's a common beginners mistake. This may be something we cannot come to an agreement on morally, but I suppose it won't really matter for the rest of the mathematical conversation which continues below.
> I didn't define it, Alan Turing did, in 1936. It's not a debating point, it's a fundamental limitation. All Turing-complete code sources have this limitation. Read more here: https://en.wikipedia.org/wiki/Halting_problem .
Wikipedia is a poor source to cite, but when I follow it I see no claim or definition by Turing for what non-trivial is. I see claim of what Rice meant by non-trivial in their eponymous theorem in 1951, but that's neither from 1936 nor a relevant definition for the current discussion so I must assume you mean somewhere else in Turing's actual paper I'd need to check.
Which takes us to the actual 1936 paper rather than Wikipedia's summary https://www.cs.virginia.edu/~robins/Turing_Paper_1936.pdf. I see 3 mentions of triviality, none of which appear to give a definition of what a non-trivial provably haltable example is:
1. Discussion of the remainder of the theorem itself being trivial [on page 31 of his paper, page 260 of the journal]
2. Since CC_0 is already been shown provable the conditional proof of the A(M)->CC_0 is trivial by the rules of implication [p32, 261 of the journal]
3. A trivial replacement of the variable naming scheme allows translation between the two notations without changing the calculus of them. [p34, 263 of the journal]
None of these seem to define what a non-trivially provable program (Turing Machine/Algorithm) is in context of the halting problem, so I again ask can you tell me where and what actual definition in Turing's actual 1936 paper you are using to define what a non-trivial program is so that I may apply this definition to the current conversation?
As another aside, one of my favorite "simplest" examples of a non-trivially provable program we know never halts despite the general case result of the halting problem:
To prove this never halts you have to prove Fermat's last theorem. Which we have, and so we know this must never halt as you iterate infinitely over the positive integers, but it took one of the most complicated mathematical proofs known to show it.There are certainly definitions of non-trivial where this is still considered trivial, but I'm at a loss to what part of Turing's paper gives such a definition.
>> This is a simple restatement of the original claim, and it is false. The program being discussed is subject to the Turing Halting Problem. The program being tested, the same. Lean, the prover and the final authority, the same. All are subject to this fundamental limitation.
> I disagree ...
This is not a topic open to debate, it is a statement of fact. I strongly recommend that you learn this topic, and the topics of mathematics and logic, where some statements can be proven true or false without ambiguity.
The Turing Halting Problem applies to all Turing-complete environments. The program under discussion meets the criterion. AI meets the criterion. Lean meets the criterion.
> There are certainly definitions of non-trivial ...
This is a logical fallacy known as "Logic Chopping" : https://iep.utm.edu/fallacy/#Logic%Chopping
> where this is still considered trivial, but I'm at a loss to what part of Turing's paper gives such a definition.
Yes, I can see that, but that's not what this discussion is about. Read this before posting again: https://en.wikipedia.org/wiki/Halting_problem
Dozens of online articles on this topic, make the same point in the same way. None of them digress into logical fallacies.
> This may be something we cannot come to an agreement on morally ...
"Morally", really? Another logical fallacy, another digression, and not the topic.
If you wish to say you have a counterclaim to the idea mistakes can be blocked regardless if every program can be proven to halt which is based in mathematical reasoning you must be able to state or produce the claim in the actual mathematical reasoning itself (or at least a link to the specific math directly relevant to the claim), not an English text summary of an entire paper/problem on Wikipedia. Anything less is not mathematical reasoning.
I'm unable to say more at this point as I can only assume you will continue to use that as a chance to quote and discuss everything but actual mathematics.
> If you wish to say you have a counterclaim to the idea mistakes can be blocked regardless if every program can be proven to halt which is based in mathematical reasoning you must be able to state or produce the claim in the actual mathematical reasoning itself ...
This is not a philosophy discussion, and Alan Turing already plowed this ground. The original claim "Bend - a language that blocks AI mistakes via proof [...]" is unsupportable.
> ... if every program can be proven to halt ...
But that's not so. You have introduced a qualifier that is known to be false.
> ... a chance to quote and discuss everything but actual mathematics.
Yes, I agree -- you should stop doing that. I keep referring to the original technical reason the original claim is unsupportable, others keep raising objections without trying to think through their positions.
It's not as though the Halting Problem is on the Millennium Prize Problem list, open to contradiction/reconsideration by some future challenge. It's a theorem, not a conjecture.
I've given notes of where in Turing's paper any type use triviality could be found, with direct page citations of the relevant original math, along with the mathematical reasons it doesn't have anything to do with the plain English statements you are making. This effort was a kindness done in good faith that I might find said mathematical definition of non-triviality for the halting problem somewhere in the paper, not something needed to show your claim devoid of a shown basis in mathematical reasoning so far. That much is apparent by the lack of a single mathematically defined claim specified by any of your messages.
That said, if you'd like me to formally show what e.g. the triviality in the rules of implication Turing was talking about are in a purely mathematical form I'd be glad to state with no English commentary out of good faith as well. This would seem a waste of time unless that's the part of the paper you think the definition of non-triviality can be sourced, but at least I'd at last have a clear mathematical claim from you to discuss.
It is now your opportunity to make a mathematical claim, of which proof by assertion this paper should apply because it proves something in general is not.
> That much is apparent by the lack of a single mathematically defined claim specified by any of your messages.
I posted the Turing Halting Problem Wikipedia page. It describes a theorem, not a conjecture that I need to prove, which shows the original poster's claim is contradicted by established facts.
Let me put it this way. If I say, "There are an infinity of primes," will you reply, saying, "I disagree"? That position would be equally appropriate -- that is to say, not appropriate at all.
Am I obliged to prove the infinity of primes by generating an infinity of candidate integers and prove that some of them are prime? No, and by the same token, I'm not obliged to reply to your naive demands and teach you why the Halting Problem falsifies the claim made by the original poster. That is not my responsibility, it is yours.
In mathematics, some things are conjectures -- the Millennium Challenge problems, for example. Others are theorems, meaning established truths, beyond dispute. Turing's Halting problem is a theorem.
Here is another authoritative reference to the fact I originally posted: "Did Turing prove the undecidability of the halting problem?" from the Oxford University Press -- https://academic.oup.com/logcom/article/36/1/exaf075/8417148 .
The question in the title is rhetorical, as you will discover if you read and understand the article I just linked.
> It is now your opportunity to make a mathematical claim, of which proof by assertion this paper should apply because it proves something in general is not.
How many more mathematical literature references will you require before you realize I have already met any burden of proof? I could post the entire technical proof here, but (a) the editors of this forum would kick me out, and (b) you would still refuse to accept the evidence.
How do I know this? Because you keep refusing to learn what you need to know to engage in this conversation.
There are an infinity of primes -- your turn.
The answer to what I'd say if this were about primes and a program which blocks outputting them in pure mathematics, despite there being infinitely many, would be (using a similar type of argument I gave early on for the current discussion):
(Apologies for the formatting, HN does not allow latex)The thing blocking me from being able to do the same here is I defined a similarly styled argument about it being possible to construct a program (glad to give it in pure math if tou'd like) which blocks all non-halting programs by only allowing ones showable to be halting (n.b. much as the above example with primes, this result did not require listing every non-halting program and so does not disagree with the general halting problem) and you said Turing's paper contains some definition of non-triviality which says why that cannot be and then refuse to say what and where in this paper you believe this definition of non-triviality to be even though I could find no such thing.
If you said Euclid showed the above proof on primes does not apply because he gave some definition of non-triviality, telling me it's somewhere in his book Elements, and I said book IX proposition 20 does not say anything like that, so you say "it's on Wikipedia"... you could see why I have doubts you have any mathematical claim to produce defining said definition. At the very least, you could see how I'd still be awaiting to hear the actual mathematics you're using.
> The answer to what I'd say if this were about primes and a program which blocks outputting them in pure mathematics, despite there being infinitely many, would be ... [ snip ] ... Q.E.D.
Now I get it. I should have realized at the outset that this outcome lay in the future. You are here to pointlessly argue, not discuss nor debate.
> At the very least, you could see how I'd still be awaiting to hear the actual mathematics you're using.
Yes -- notwithstanding that I have posted links to that exact evidence from multiple sources. The problem is not a lack of evidence, the problem is that you refuse to read it.
On that topic, here is a link to Alan Turing's 1936 paper -- 36 pages long: https://www.cs.virginia.edu/~robins/Turing_Paper_1936.pdf
Andrew Wiles conclusively (dis)proved Fermat's Last Theorem. If you disagree, and since you have demonstrated a willingness to disagree with anything, I would have to post a link to the evidence, not the evidence itself, because the (dis)proof is 129 pages long.
As I post this, I'm trying to imagine the corpus of mathematical knowledge you're unwilling to accept, because it won't fit into a finite-sized Hacker News post -- relativity, both special and general, quantum mechanics, dozens of others.
I'm also trying to imagine someone whose literacy filter consists of "Tl;DR!"
It truly breaks my heart to see any of the math snipped out yet again. You sound more than capable of formulating your assertions in pure math but seemingly refuse to state it that way, which feels like watching a bright light in the world going out as it seeks to avoid rigor.
A set of theorems (of which I accept all you've named) without the definitions of exactly how and why they apply to the give problem is no more mathematics than a bunch of bricks is a chimney. I believe all of these beautiful proofs, I just don't believe you've properly demonstrated you can build your chimney with them. If you ever wish to build the chimney I'd be ecstatic, until then I think I don't think anything else can be said about how the pile of bricks aren't an example of one - especially if you're going to give the URL I already provided you when asking where the definition of the connection in it was https://news.ycombinator.com/item?id=49761146
I do wish you well and I'm sorry if my requirement for rigorous statements in math seems pointless to you. It's something I hold dear. I'll keep notifications in my script enabled in case you do want to start discussing the math rigorously, but I'll no longer try to convince you that's what's needed for your claims to hold mathematical weight anymore or any of the other things which seem to be bothering you for no gains.
> A set of theorems (of which I accept all you've named) without the definitions of exactly how and why they apply to the give problem is no more mathematics than a bunch of bricks is a chimney.
A second reply. What you're not getting is that the mathematical equations in Turing's paper don't make its point. There are plenty of equations, but the paper's meaning lies in its logical arguments, for which the equations can only play a supporting role.
If the equations are taken out of the paper and presented separately, as you have repeatedly demanded, the paper's thesis falls apart. But to understand this, you would have to read the paper itself and absorb Turing's logical arguments. And the paper can't be made shorter without losing its meaning.
More evidence for this is given by the fact that Alonzo Church published a similar paper in 1936, different author, different equations, but the same logical argument and conclusion, such that Church and Turing are now given equal credit for the basic idea -- an idea that is supported by equations but not provided by them (https://courses.fit.cvut.cz/MI-VYC/church-a-note-on-the-ents...).
This is true in many parts of mathematics and logic. Another example is Einstein's 1905 paper later identified as the source of "special relativity". If you remove the equations and present them separately, all meaning is lost. In fact, in that case, the actual meaning of a particular equation was lost to Einstein himself, but that meaning occurred to his former math teacher Hermann Minkoswski, who went on to publish about something Minkowski called "spacetime". As before, the equations didn't convey the paper's real meaning, they could only play a supporting role. About this outcome Einstein later said, "Since the mathematicians have invaded relativity theory, I don't understand it myself any more."
Another more recent example is the recently solved "Navier–Stokes existence and smoothness problem" as it was titled by the Clay Mathematics Institute. The equation is easy to render, but as with the other examples, the problem to be solved goes far beyond the equation itself, and the meaning of the recent result lies not in the equation, but in its treatment and processing by AI.
In Navier-Stokes, everyone had access to the equations, but until recently no one could answer a fundamental question about it, and as with the prior examples, the real meaning requires one to read the articles that provide the logical reasoning. In each of these examples and many more, listing the equations can only be a preliminary step to true understanding.
More importantly, the meaning of the papers cannot be summarized in fewer words than are provided by the papers themselves. Mathematicians don't go out of their way to make their papers longer than their contents require, in fact, quite the opposite.
I can't believe you're still expecting bumperstickers to stand in for technical articles. As before, you should read the original articles instead of complaining that they're too long for your limited attention span.
> There are plenty of equations, but the paper's meaning lies in its logical arguments
This is the difference I feared. I trust, understand, and take lead of the rigorous math of the paper, you opt to follow in English arguments of what you think it's supposed to mean or apply to. No matter how much math is discussed, it'll never lead to anything if that's not where your understanding of the paper comes from.
It's one of the main things which separate hard sciences from things like Psychology where anyone can just talk about what they understand/see or want to link instead of define it in logic itself, and I must admit I've never believed much of the soft sciences because of that lack of rigor. Maybe that rejection of soft science as truth is a limitation of mine :) but I don't see myself abandoning the view any time soon.
> It truly breaks my heart to see any of the math snipped out yet again.
A false statement. I posted a link to the evidence, which cannot be summarized to satisfy your short attention span. Your unwillingness to read it only reveals your shallow grasp of modern technical topics.
Here is a short list of topics that cannot be converted into bumperstickers, your preferred medium of expression:
This list is by no means complete, but the last entry overlaps with the topic of this conversation, for reasons that will not be obvious to you unless and until you overcome your distaste for evidence.> I do wish you well and I'm sorry if my requirement for rigorous statements in math seems pointless to you.
Excuse, me, what? I have posted links to the evidence that proves your position to be false, but you won't read it. You are to modern times what a religious fundamentalist is to science -- the primary obstacle to human progress.
Am I saying your unwillingness to absorb ideas outside your short attention span is itself an obstacle to human progress? No, actually, I'm saying you should avoid drawing conclusions without first examining the evidence.
It isn't only that you won't read the evidence that proves your position to be wrong -- that is simply sad, not fatal. It is that you draw conclusions without first examining the readily available evidence.
> A set of theorems (of which I accept all you've named) without the definitions of exactly how and why they apply to the give problem is no more mathematics than a bunch of bricks is a chimney.
Wow. You just dismissed the validity of all the topics in my list above, each of which produce everyday valid conclusions derived from very complex logical and mathematical antecedents.
Get professional help.
> The halting problem applies to all systems able to perform Peano arithmetic.
You're confusing the halting problem with Gödel's first incompleteness theorem.
And Bend is just claiming to be sound but incomplete
> You're confusing the halting problem with Gödel's first incompleteness theorem.
So did Alan Turing, but ... he wasn't confused. The two are connected.
> And Bend is just claiming to be sound but incomplete
That is not what was said. Here it is:
"Bend – a language that blocks AI mistakes via proof."
That's not possible, and changing what was claimed is not productive.
You are the one being insufficiently precise here. There would only be fundamental obstacles if there was an additional claim "allows all correct programs".
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.
> 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".
I like it. It's like Bogosort- the Language. It would work much better if a) tokens were free and b) computation, therefore retries, didn't take any time at all. In the current world it's going to be fun watching LLMs getting stuck in infinite loops, doing and undoing their work to try and uphold a law they don't know how to uphold.
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?
It's formal verification that works with proofs. Like coq, agda, lean, with which e.g. they proven the Navier-Stokes. This is a new such language.
Assertions and constraint programming is often runtime only. These languages use dependent types and verify the proves at compile time.
It's not exactly like a proof assistant because it has a built-in generate-and-test loop: an LLM generates code until the code passes verification.
Basically that's all of AI nowadays: generate-and-test loops. It's like the 1950's all over again.
“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.
Yes, we need both.
This seems less like a proof and more like a "pretty please" with test cases?
Weird claim about us living in a post-AGI world, no company has shown true AGI yet.
I see no such claim.
> In the post-AGI economy
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.
All these skeptics and nobody just tried it out?
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?
> All these skeptics and nobody just tried it out?
Welcome to HN!
May I remind you of the Dropbox comment? https://news.ycombinator.com/item?id=9224
Classic. That comment should be in a museum.
Without debating the general topic, I think it's important https://news.ycombinator.com/item?id=27068148 be shared any time the above is.
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.
I gave it a spin using muse 1.3
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.
Giving it a paradox yields interesting results. I'm not sure what its proving other than there will be cases that proofs can't help you with. I can't think of a practical example.
"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"
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
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
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):
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.
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
3. Is the GPU used at both runtime and compile time?
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.
Hey, I get a 404 from that link.
fixed ty
Funny seeing you here--I'm in 590 with Max and Eric. I saw Agda and guessed it was someone from the group :)
Victor Taelin has been doing interesting PLT research for 10+ years.
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
This is a very strange comment
First, I think everything I said was respectful and rooted in the content of the Bend page rather than an assault of Victor as a person. I’m very confused by your random appeal to the author’s reputation here. He seems like a smart and cool dude, and I still have things to say in response to what’s presented here for Bend
Second, the paper is openly written by Fable 5.1, so I’m not making any unfounded accusations
Victor put 5+ years of research into this. You can find many of previous versions (which use different approach, do a different kind of a thing, etc.) on the github. "Bend2" in particular have been in development for 2 years.
Calling this "a random vibecoded project" is rather disrespectful, don't you think?
Regarding the paper, he states it clearly "designed by the human author". That's not at all the same as just asking Fable to write a paper. I mean the important thing is ideas, not the way they are described.
Please tell me how "I'm glad you're having fun vibecoding" is not disrespectful?
I thought that you thought Bend web site is all that is to it and wanted to point to relevant information. But if you think that "having fun vibecoding" is an appropriate thing to say to somebody who spent many years doing research, I don't know what else to say.
Again, as a "proof of research" take a look at : https://github.com/VictorTaelin/Interaction-Type-Theory that's 3 year old, pre-dates Fable, but OMG doesn't look like a paper.
Again, very strange
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
> 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.
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...
How do you know the implementation is complete or that it works well?
Have you evaluated it?
Wouldn’t you be inclined to withhold any claims of anything being substantiated until it’s actually been evaluated?
Wait what? Have you? Why are you posting passive aggressive unfounded dismissals posing as questions?
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?
No, I have not, so I don’t post baseless dismissals. I don’t call authors sus af and I don’t call people’s work vibe coded slop.
Have I?
Are you arguing with me or the parent who actually called it “sus af”?
To pick on a few examples:
> 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.)
stschaef‘S comment was on topic and a critique (albeit sharp) of the work.
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”.
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.
The author was very polite to even reply at all.
> Your comment is a personal attack
I don't think stschaef is a bully; in fact, if my guess that he's a researcher is correct, I think he's likely highly altruistic (I've never met him, but categorically, researchers are people who chose a difficult, low-paying job doing work of great societal value).
However (again if my guess is right), I think he could easily be in an environment where narratives about people's work being worthless, about them being stupid or unserious or otherwise beneath consideration, are common. It's a reaction to the fact that in any field, the amount of research produced is overwhelmingly more than anyone can digest. There's a lot of unstated anxiety and guilt about that, on the side of both writers (who worry no one will read their research) and readers (who feel obligated to try to read everything and are eventually, inevitably overwhelmed), which IMO is itself a product of the basically altruistic nature of most researchers.
The overwhelming reality of being a researcher is an inescapable, empirical fact, but the narratives people create around that reality, about peoples' work and its worth, are not. People are hard-wired to be sensitive to rejection, because humans are a cooperative species and social acceptance is existential to each of us, and the problem is that a lot of researchers, who are steeped in these narratives, are trapped in a self-reinforcing cycle of community attachment threat: their research sucks (or could start to suck if they ever went on vacation), and the research of most of the people who are evaluating them sucks too.
What if these stories about the worth of people and their work aren't true? Guess what: one can do amazing research and it still goes nowhere, because ultimately it's not possible to control other peoples' behavior. If one's goal in research is acceptance and respect from the community, they should consider that they're gambling their time, energy and youth on an outcome they can't control. The research community can be a fine place, but it's not special—one does not have to be a researcher, and if the experience of being a researcher sucks for them, they should quit, because living a good life is their responsibility.
I grew up around this attitude, and children are particularly sensitive to attachment threat. It's bad enough that researchers tell these stories about each other, but once these narratives and communication patterns about peoples' work and its worth leak outside the context of the research community, they run right into the reality of human attachment and the expectations of communities that aren't the research community. I'll say about my own family: I think they were good people who learned an unhealthy, judgmental attitude (towards themselves as well as others). I think they immiserated themselves (and inevitably the people around them), because perpetual attachment threat had traumatized them into false sense of obligation, and I wish they had quit.
Even if one stays, they should understand the mismatch between the narratives and culture of the research community, and they needs and expectations of most people outside of it. That was the context of my comment. I think it's fine if stschaef doesn't like TFA and doesn't find Bend novel or interesting, but my analysis of the sentences quoted reflected my organic reaction to them, and I stand behind it and my other feedback.
Commit history is back!
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
[dead]
> In the post-AGI economy, humans will eventually stop writing and reading code
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"?
> In the post-AGI economy, humans will eventually 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
Is there an overview on how this works? E.g. if we code a contract in LAWS.bend, how is it enforced? What prevents my LLM model to skip a contract?
I believe it works like this:
- 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.
Blocked the a few attempts I tried, usually by changing the amount of fencing:
- 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!
Well, didn't win, but definitely broke it. Needs an edge case handler for tool call exhaustion:
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'm interested in how to integrate formal verification with existing software libraries. For example, https://github.com/verus-lang/verus integrates proof with macro in Rust. What's the plan for Bend?
Thanks for your time.
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."
Yeah, but this assumes the llm will follow the "Laws". I find llms routinely ignore steering docs etc, even outright instructions. Like "Dont use python", next line it is trying to use Python.
Seems to me the llm will just try to work around the "laws"
No, it doesn't assume that. It simply assumes that you can verify whether or not the LLM's implementation adheres to the laws you defined up-front — which it does not if it modified the laws.
Exactly, you can have all the laws, but an LLM (or even a human) will just delete or refine the laws and hide the change in a 5kloc PR, that the "code author" will not review carefully, and you have 5 min to review and stamp to make sure your company is moving fast...
If the LLM changes the laws to bypass them that's on you. The whole point of this is that you don't have to manually review most code written; only the laws. If the LLM changes the laws and you ignore it that's a you problem.
I totally get it, but in companies where you gotta crunch out 10x more features, review 10x from other people, this could be easily overlooked.
This is great. I can't imagine why would anyone be unappreciative of this. Since AI is going to be here anyway, why not make it safer and more useful?
However, this also means acknowledging that AI will never be error-free (which is the truth; all AI is heuristics-based).
20K stars and a single commit an hour ago?
How many goats were sacrificed?
Genuinely wondering where this dark magic came from.
Presumably the repo was force-pushed (breaking all clones and forks in the process).
Qualityeesh!
Trending idea! On the same subject, but aimed at compatibility with TypeScript, I just discovered Code Contracts.
https://code-contracts.cc/
this almost feels like a monkey paw scenario, where poor laws can fundamentally alter things in a way that is surely not intended.
"make the board 1x1"
and the flag is placed off the board... i feel like i would blow my foot off with this.
"make the player teleport to square 1,1 on move and the flag stay at 1,1" the LLM put the flag at 1,0. Not sure if this is the intent.
What’s the difference between a law and an integration test?
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.
Exactly. If humans were good at writing proofs, they'd just write the code.
But how does it do on the balls benchmark???
https://benjdd.com/languages/
good question we'll try
I'd like to hear how this compares to Ada/SPARK.
I tried insisting that the bug and the walls were on different planes of existence... But then the flag gained "phase lock" and blocked me.
why there is no LAWS.bend in the bend repo to verify the correctness of the repo? like some of the C compilers are written in C
You just need to split apart "Wall is stop".
Bend might reply with "Flag is wall".
Seems they might have discoveref the language of G*d:
"[...] he has given a law to which they must conform."
- Psalms 148:6 (CJB)
:)
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'd like to see it try and ensure the law "The program must halt"...
Oh I'm sure OpenAI or Anthropic will vibe disprove Turing any day now!
have been following bend's development via x for some time - congratulations on the release!
https://github.com/bendlang/bend
...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.
Multiple times, even. Still no real reason why. https://github.com/bendlang/bend/activity?ref=main
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...
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?
Commit history is back!
Taelin's X is a war story of how the codexes and fables tried to bend it. If you're afraid then LLMs were used in there - fear no more - they were.
> curl -fsSL https://bend-lang.com/install.sh | sh
Hmmm... needs `sudo`.
GitHub shows 44 contributors. 41 distinct users have merged pull requests.
...so now their work has been reduced to nothing?
Old repo can be accessed here https://github.com/HigherOrderCO/Bend1 . I guess we could have it as a branch on the bend2 repo
yes, there's a lot of personal info and AI slop in the commit history.
is this a problem to you? why
To give you a concrete reason why you should care to preserve the exact history and why it’s a matter of trust: in your paper, you reported the pinned SHA head of the benchmarks you ran. 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?
https://github.com/bendlang/bend/blob/80b6539bc57621633ca68e...
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.
> 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.
alright, we could try to restore history removing sensitive bits if that's so important. thanks for the feedback
Props. G'luck with your project, I know what it's like to work nights & weekends. Unfortunately, first impressions matter.
Ty! Commit history is back now
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.
Why would anyone want to work with such a dystopian setup? Prove your code directly in Lean or Coq or leave it.
Most of that is just the test suite. The actual code is about 10k lines
SupGen isnt the backend to the type system? to auto implement the laws?
[dead]
Interesting... But I don't think formal software verification is going to be the answer (is that what this is? Kind of unclear.)
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.
Is EC2 real-world enough? From June:
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...
Funny you say that while OpenAI and rest of the world rely on Lean and other formal systems to power through (or sometime brute force) math problems.
Very interesting business model: a custom paid agent for updating proofs faster.
Why wouldn’t you use dafny?
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?
No windows? axiomatic F32? I'll stick with Slopjective-C 3.0 thanks
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.
What exactly enforces that an AI follows these rules?
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.
Taelin is the beast! The best of Brazilian tech.
so we stop developing code, to develop code again...
I wish this can be a extension of existing languages.
Great team behind it. SSL cert is quantum resistant even.
Aren't ALL type system proof systems?
Well, yeah. Most are just unsound and not too useful (e.g. can only state propositional logic statements).
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.
Is Bend built on the HVM? or no?
Sounds like hoare logic to me?
2 wrongs will never make a right
Sometimes two falses equal true, and three lefts make a right.
How is that better than just writing tests and running them in any other language, let's say Go?
Tests aren't proofs.
A single commit in github, and the compiler isn't there anyway. Where is the compiler?
I’m just looking at it for the first time myself, but isn’t the compiler in https://github.com/bendlang/bend/blob/main/bend2/comp.ts ?
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.
the compiler is in comp.ts, alongside the runtime
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)
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.
Have we delegated writing code to "AGIs" so we can write code to proof that the slop code works? I have a vague memory of pre-AGI era, when we wrote things called "tests" to verify that our code did what it claimed to do.
.
The benchmarks: https://github.com/bendlang/bend/tree/main/bench
The script we use to run them on our servers: https://github.com/bendlang/bend/blob/main/gates/perf.ts
Read the damn code and readme, for god's sake!
Not the AI slop background colour T_T
It's just solarized, i imagine most developers are familiar with it
[flagged]
20k stars is sooooooooo sus lmao
He got 80k+ followers on Twitter (x), tracking his progress on Bend, why sus?
20k stars is about the same as Crystal and Gleam, languages with actual user bases that have been around for years. Here’s what organic versus… we’ll say viral growth looks like.
https://www.star-history.com/?repos=bendlang%2Fbend%2Ccrysta...
Awesome! Now we can use AI to manage our nuclear defense and attack response.
[flagged]
As I understand it, there are no implicit arguments (and, consequently, no unification) here, right? This doesn't seem very serious given the ambitions of a project like this. Of course, one could argue that it isn't necessary if everything is generated by a LLMs, but… why bother with "human-readable" Python-like syntax in that case? It's not Python, after all, and I don't think it would help with LLM code generation in any way.
And benchmarking this language against Isabelle/Agda/Lean/Rocq is strange. The time taken for those systems to perform their checks is mostly spent on elaboration, which includes unification against metavariables, typeclass resolution and tactics. Bend has none of that (there are no type classes or traits, and according to the README, everything must be fully annotated and nothing inferred). This means that the benchmark is comparing Bend's checker to the other systems' elaborators + kernels rather than their kernels (Agda doesn't have this separation though). The latter would be a fairer comparison, and in this area the other systems are already fast. Framing it as "outperforming every proof assistant" without that caveat is misleading.
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.
[flagged]
[flagged]
[flagged]
[flagged]
[flagged]
[dead]
[dead]
[dead]
[dead]
[dead]
[dead]
[dead]
[dead]
[dead]
[dead]