I'll try to sanitize the commit history, I had no idea it would be so important
2,083 karma · joined September 27, 2015
It works like this: if you prove that a property about natural numbers holds for 0, and if you also prove that, assuming the property holds for N, it also holds for N+1; then, you can conclude the property holds for every N, up to infinity. This is a bit of a mouthful, but the logic holds.
Induction is the one trick that makes all of mathematics (as we know it) possible, and it also applies to software. So, for example, to prove that no move leads to an invalid state, we prove that the initial state is valid, and then prove that, given a valid state, applying any event won't return an invalid state.
And that's it actually.
Of course, once you have an app with hundreds of actions, proving that no action leads to an invalid state requires a lot of these "induction arguments". But not infinitely many, because there is a finite amount of "infinite paths" that a real software can take. So, that's what the AI does. It proves, by induction, that none of these "infinite paths" that an app can take leads to an invalid state. And this convinces the compiler that invalid states are impossible.
Theorem proving in Bend is a dance between the prover (the model) and the compiler (the checker); a machine trying to convince another machine about properties of infinite states. And that's is kinda poetic, don't you think?
You can find it on Bend's demo directory in our GitHub.
Don't tell anyone though!
So, yes, that's the issue with laws: they only protect what you remember to write. They're not a silver bullet. But they can still be incredibly useful, because it takes a small law to protect against entire classes of bug, covering your entire codebase. For example:
LAW: "the sum of all balances in this contract must be zero"
This one liner would have prevented Ethereum's infamous "The DAO" hack, where millions were stolen and almost undermined the entire project. But if your laws are under-specifying or ill-specifying your intents, Bend can't do anything to protect you.
If you mean about the type theory specifically, "Type Theory and Formal Proof by Nederpelt and Geuvers" is a good introduction. Not sure what I'd recommend on linear types, no book I know of is very introductory? Perhaps "Idris 2: Quantitative Type Theory in Practice", which is a language with similar foundations to Bend, and the author wrote a book on it (and inspired myself!)
It just means that Bend compiles to a single .c file, and that file compiles to either Metal or CUDA, via macros, depending on your target. This shouldn't be relevant to most users. It is just a way I found to keep the file small and reuse as much code as possible, rather than rewriting the runtime 3 times (once for C, once for Metal, once for CUDA).
`-` 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!
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.
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)
is this a problem to you? why
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!
For example, if you search for `Integer -> Integer -> Integer` function, it will consider Integers of different bit-sizes. But if you instead search for `∀(n: Nat). Int(n) -> Int(n) -> Int(n)`, you will only consider integers of the same bit-size, which is a much smaller space. You can make arbitrary restrictions to shorten your search.
It works by enumerating ALL possible functions and running them. Obviously, that naive approach is exponential, so, the entire point is whether we can apply some clever tricks (based on optimal evaluators) to make this search "slightly less intractable".
So, to answer your question directly: if you asked it to design a prime number generator, if it found anything at all, it would probably be a simple, slow trial-and-error algorithm, or something in these lines.
https://x.com/VictorTaelin/status/1819774880130158663
That's as much as I can share for now though
And that's comparing a first-version interpreter against a SOTA runtime deployed in all browsers around the world and optimized by all major companies over 20+ years. If that's not useful to you, that's useful to me, which is why I wanted to share so it can be useful to more people.
Just a note: we are NOT 10x slower than Python. I think a lot of people got the wrong message from this thread. HVM is actually quite fast already. It is just that, on this specific program, Python was doing no allocations, while HVM was allocating a lot.
If you compare programs that do the same allocation, HVM already outperforms not just Python but even compiled languages like Haskell/GHC, due to using all cores. See the Bitonic Sort example. And that's extremely relevant, because real world programs in high-level languages allocate a lot!
I think I made a huge mistake of using a "sum" example on the GUIDE, since it is actually one of the few specific programs where HVM will do poorly today.
I truly want to help here, but that is like asking us to tell you how many gallops per second hour car does. It just makes no sense in context. If I did invent some conversion, I would be lying, and that would be much worse than using a non-familiar term. The way to compare across languages is to benchmark and report on time. Which is like "horsepower" in that sense, as it applies to both domains.
A GPU core (shading unit) is 100x weaker than a CPU core, thus the difference.
ON the GPU, HVM's performance scales almost 16000x with 16000x cores. Thus the "near ideal speedup".
Not everyone knows how GPUs work, so we should have been more clear about that!