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

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!

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.

GitHub shows 44 contributors. 41 distinct users have merged pull requests.

...so now their work has been reduced to nothing?

yes, there's a lot of personal info and AI slop in the commit history.

is this a problem to you? why

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.

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

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.

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

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.

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!

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?

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)

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.

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!

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!

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.

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?

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

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.

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!

  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.

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

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

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.

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

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

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