I’m just looking at it for the first time myself, but isn’t the compiler in https://github.com/bendlang/bend/blob/main/bend2/comp.ts ?

the compiler is in comp.ts, alongside the runtime

it is not a pretty file and it has a lot of gambiarra and AI slop for now

if you want to read something worthy, read the kernel (bend.ts)

Then you might be interested in Marc Thatcher's recent PhD thesis dedicated to interaction nets [1]. A great exposition of interaction nets through multiplicative linear logic's proof nets, and several novel contributions like productivity analysis for interaction nets.

[1] https://hdl.handle.net/10779/uos.32024301

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

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

Taelin's X is a war story of how the codexes and fables tried to bend it. If you're afraid then LLMs were used in there - fear no more - they were.

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

is this a problem to you? why

curl -fsSL https://bend-lang.com/install.sh | sh

Hmmm... needs `sudo`.

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

Is EC2 real-world enough? From June:

https://aws.amazon.com/blogs/compute/aws-nitro-isolation-eng...

And for the PQ parts of Apple's crypto libraries, from May:

https://security.apple.com/blog/formal-verification-corecryp...

Similar from Microsoft, from July:

https://www.microsoft.com/en-us/research/blog/verifying-rust...

Words of wisdom.

true

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.

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

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!

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.

1. The paper explains it well:

https://github.com/bendlang-private/bend/blob/main/paper/Ben...

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?

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.

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

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

  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.

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

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.