bend

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

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.