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.

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!

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

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?

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?

Congrats, Victor!

É ótimo ver um brasileiro criando algo tão único!

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)

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.

Glad to see this finally released! What are you doing next?

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.

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!

what happened to your other project? HVM?

honestly just Bend is a great HN title, you can describe it more concretely on the homepage

Speaking of lava, you should do a presentation to the local tech group if you're ever here in Bend, Oregon...

[dead]

[dead]

[dead]

[flagged]