Thread

1. LightMachine · 1789679503 · focus · HN ↗

   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!

   1. avodonosov · 1789681364 · focus · HN ↗

      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)

      1. LightMachine · 1789682639 · focus · HN ↗

         There isn't a single book that covers all of it... Bend's theory touches various domains (dependent types, substructural types, termination). And then there's the runtime, compiler, GPU kernels...

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

         1. avodonosov · 1789684167 · focus · HN ↗

            Thank you.

            1. avodonosov · 1789734936 · focus · HN ↗

               Maybe you can explain or give a hint, why a function that never returns could prove anything?
         2. alew1 · 1789700973 · focus · HN ↗

            Does Bend have linear types? I didn't see anything on them in a quick skim of the GUIDE file.

            1. LightMachine · 1789702037 · focus · HN ↗

               the entire language is based on linear types! it says so in the GUIDE yes

               1. alew1 · 1789716226 · focus · HN ↗

                  Ah, thanks, was looking at the readme instead of the guide

Unofficial Hacker News client; not affiliated with Y Combinator.