Bend – A language that blocks AI mistakes via proof, on CPU and GPU

boxed

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

tyushk

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!

AlexErrant

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 .

IshKebab

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.

garrisonj

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

v9v

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

LightMachine

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!

stschaef

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

amluto

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) 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? At this point I stopped reading.

hirako2000

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

monster_truck

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

12uq7

claude: 1 commit 1,722,119 ++0 -- I assume that Claude formally proved Bend correct like CakeML? Why would anyone want to work with such a dystopian setup? Prove your code directly in Lean or Coq or leave it.

giancarlostoro

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

hollowturtle

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

docheinestages

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.

resonious

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?

RomanKornev

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

fudged71

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

npn

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.

gigatexal

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?