Bend: a language that blocks AI mistakes with mathematical proof

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.

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.

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.

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

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"

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