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!

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)?

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.

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.

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.

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"

> 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.

The issue is I’ll have to vibecode all the laws and the laws could be wrong.

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!

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.

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?

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

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.

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?

Trending idea! On the same subject, but aimed at compatibility with TypeScript, I just discovered Code Contracts.

https://code-contracts.cc/

Congrats on the launch!

Question, does the parallelism work on M-Series GPU? The page says CUDA parallelism but shows Mac performance numbers.

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.

> 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.

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.

This seems less like a proof and more like a "pretty please" with test cases?

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

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."

“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.

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!

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).

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.

I wish this can be a extension of existing languages.

so we stop developing code, to develop code again...

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:

    def length(a, -A: Kind(a), xs: List<a, A>) -> Nat:
      match xs:
        case Nil{}:
          0n
        case Con{h, t}:
          1n+length(a, A, t)

- I don't understand the Array example:

    import Base
    
    def main() -> Array<U32> & U32:
      a = [0 : U32*8n] # new array with 8 copies of 0
      a[5] <- 42       # performs an in-place rewrite
      a[5]             # reads index 5

- I don't even understand the Array explanation:

> The slot count after * is a power of two; [0 : U32^3n] names the depth instead.

Okay, the 8 in *8n above is indeed a power of two. Does the language require it? Does it actually mean 2^8? What is the "depth" of an array? Does this language not have non-power-of-two-sized arrays?

At this point I stopped reading.

Weird claim about us living in a post-AGI world, no company has shown true AGI yet.

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.

But how does it do on the balls benchmark???

https://benjdd.com/languages/

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.

You just need to split apart "Wall is stop".

20K stars and a single commit an hour ago?

How many goats were sacrificed?

Genuinely wondering where this dark magic came from.

I'd like to hear how this compares to Ada/SPARK.

have been following bend's development via x for some time - congratulations on the release!

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?

Very interesting business model: a custom paid agent for updating proofs faster.

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.

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?

Why wouldn’t you use dafny?

No windows? axiomatic F32? I'll stick with Slopjective-C 3.0 thanks

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.

2 wrongs will never make a right

Great team behind it. SSL cert is quantum resistant even.

  claude: 1 commit 1,722,119 ++0 --

Why would anyone want to work with such a dystopian setup? Prove your code directly in Lean or Coq or leave it.

How is that better than just writing tests and running them in any other language, let's say Go?

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?

.

Not the AI slop background colour T_T

Awesome! Now we can use AI to manage our nuclear defense and attack response.

20k stars is sooooooooo sus lmao

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.

A single commit in github, and the compiler isn't there anyway. Where is the compiler?

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.