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. TimTheTinker · 1789681167 · focus · HN ↗

      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?

      1. LightMachine · 1789681632 · focus · HN ↗

         The check is happening in between the animations. When the AI edits the code, Bend will check if all laws still hold, mathematically so. If not, the AI repeats, until that's the case. So, the animations just show what happens to the app with and without Bend's involvement.
   2. mmoustafa · 1789681183 · focus · HN ↗

      honestly just Bend is a great HN title, you can describe it more concretely on the homepage

      1. throooooo · 1789726240 · focus · HN ↗

         Thank you for being honest.
   3. 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
   4. ble · 1789681448 · focus · HN ↗

      I like the idea of a language intended from the start to be proved and it seems very compelling given coding agents. It's a good idea that others don't see coming -- so expect it to be frequently misunderstood and even verbally abused!
   5. gslepak · 1789681631 · focus · HN ↗

      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.

      1. LightMachine · 1789681705 · focus · HN ↗

         I will improve that phrasing, thanks.

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

   6. pdpi · 1789681723 · focus · HN ↗

      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.

      1. pixl97 · 1789682385 · focus · HN ↗

         Heh, We're writing Asimov in real life after been warned to decades.
      2. thomasfromcdnjs · 1789682483 · focus · HN ↗

         Well described the problem scope.

         I wonder if harness-hooks + Jev (equivalents) could semantically lint for `sloppy_law` etc when ever they are edited

      3. abraxas · 1789682557 · focus · HN ↗

         > writing the laws becomes a bigger problem than writing the code itself.

         Of course because at its limit programming is basically defining desired behaviour under all circumstances and logical conditions.

      4. [deleted] · 1789682829 · focus · HN ↗

         [deleted]

      5. [deleted] · 1789682856 · focus · HN ↗

         [deleted]

      6. LightMachine · 1789682947 · focus · HN ↗

         Exactly, "you can't win" is grossly under-specified. The goal of the demo is just to show that laws can't be broken. Yet, if that's your only law, the AI can do whatever to protect it - including changing how the character moves, or even removing the flag entirely!

         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.

         1. skissane · 1789688041 · focus · HN ↗

            Thought about automated discovery of laws in an existing codebase?

            If you can find a law which the existing code obeys, and show it to a human, and if they agree, save it. And maybe the AI could make a decent guess as to what kind of laws would appeal to a human versus which wouldn't – a simple law identifying a fundamental constraint the system obeys is good, something really complicated or constraining something coincidentally true isn't

            Or some kind of measure of coverage? you'd never want 100% – then your laws would become so complex you couldn't follow or maintain them – but if it is very low, that can be a signal to increase it

            1. drfloyd51 · 1789695236 · focus · HN ↗

               Discover the laws in a current code base?

               They are usually in the “tests” folder.

               So anything capable of extracting unit tests is extracting “laws”.

               One might consider the test name the text of a law. And the AI fills in the details.

               1. skissane · 1789697260 · focus · HN ↗

                  I don’t think that’s right.

                  Unit tests check whether a specific code module is implemented correctly given its (implicit) specification.

                  Good “laws” are independent of the structure of the code.

                  Tests may be a useful source for inferring what the laws are, but much of the actual content of the tests aren’t “laws” at all.

                  1. serf · 1789707548 · focus · HN ↗

                     I think the premise is more that if one is given a grouping/constellation of unit tests that one can derive generalized laws by looking at what behavior those tests were checking for or against.

                     if there are a dozen unit tests trying to determine if some regex can escape a sensitive area, then one can derive a generalized 'don't let the regex escape from here' type rule -- or at least you could theoretically. I'm sure in reality that'd be a big minefield much like harness self-skill-writing has been.

                  2. schlich · 1789731011 · focus · HN ↗

                     you might be interested in property-based testing, which somewhat enumerates tests based on invariance and induction
               2. actionfromafar · 1789722264 · focus · HN ↗

                  From the codebases I have seen the "laws" are scattered between unit tests and lots of little tests and assertions in the actual code, plus cultural norms and "do it like this" patterns.

                  But a good start could be found in the unit tests.

         2. DeusExMachina · 1789730984 · focus · HN ↗

            > LAW: "the sum of all balances in this contract must be zero"

            What prevents AI from writing an arbitrary calculation that makes sure that sum is always zero while breaking a whole other bunch of assumptions?

            If the answer is more laws, then this does not address the parent comment.

            1. Isinlor · 1789744681 · focus · HN ↗

               Gross, obvious exploits can be easily picked up by AI reviews.

               1. yencabulator · 1789753560 · focus · HN ↗

                  And then the agentic loop over the reviews will rewrite them into less obvious exploits.
               2. DeusExMachina · 1789754133 · focus · HN ↗

                  What AI reviews? I thought AI needed to be bound by Bend laws.

                  The AI either knows what the user wants perfectly and is able to prevent problems, or is a rougue agent that needs to be bound by laws to not misbehave. You can't have both.

      7. konart · 1789683109 · focus · HN ↗

         > writing the laws becomes a bigger problem than writing the code itself.

         But that's how it is anyway, no?

         Defining clear boundaries and clear goals is the hardest part. If you get those right everything else is rather trivial.

         1. bdelmas · 1789731567 · focus · HN ↗

            Well if possible you want an AI that understand the spirit of what you are asking for and will add all the missing stuff, instead of an AI that just want to hack its way to the result. Kinda what Fable brought to the table. For instance as a simple example I ask it to change the text that shows the email of the user by his name and Fable did all the code in case there is the family name missing etc. That this last part you want an AI to do. Helping you to build the system with you and not gaming what you ask for for reward.
      8. tonic_note · 1789684165 · focus · HN ↗

         Yeah all of these attempts to try and control AI outputs by using language fail to grasp that language is itself the problem. It is a closed system with no ground truth. Words only point to other words in an endless self-referential chain. There is no "closure" in language, ambiguity cannot be erased.

         Imo LLM researchers would benefit a lot by reading what continental philosophers have said on the topic of language. Barthes, Sarte, Deluze, Derrida, et. Al have a lot to say that explains why we're running into the same problems over and over.

         1. fortzi · 1789684316 · focus · HN ↗

            Natural language is ambiguous. Specifying exactly what you want in a way that is truly verifiable is the act of coding.

            1. frank00001 · 1789704152 · focus · HN ↗

               Start printing the t-shirts!

               1. shakna · 1789715488 · focus · HN ↗

                  You mean t-shirts of this comic, from 2016?

                  [0] <a href="https:&#x2F;&#x2F;www.commitstrip.com&#x2F;en&#x2F;2016&#x2F;08&#x2F;25&#x2F;a-very-comprehensive-and-precise-spec&#x2F;" rel="nofollow">https:&#x2F;&#x2F;www.commitstrip.com&#x2F;en&#x2F;2016&#x2F;08&#x2F;25&#x2F;a-very-comprehensi...

         2. krapp · 1789686595 · focus · HN ↗

            I think LLM researchers understand how LLMs work and what the limits of using natural language as an interface are. The problem is everyone else thinks they&#x27;re basically magic, expecting them to be infinitely intuitive but also strictly deterministic, like the computer from Star Trek.

            1. actionfromafar · 1789723232 · focus · HN ↗

               The computer from Star Trek sounds like it could entirely plausibly have been made with LLM components and a century of harness tweaking piled on.

               1. krapp · 1789734769 · focus · HN ↗

                  Plausibly based on what? The computer from Star Trek wasn&#x27;t real. It was Majel Barrett talking into a microphone. You can no more extrapolate any real world computer architecture from that than you can determine amphibian evolution from Kermit the Frog.

                  1. hannasanarion · 1789738130 · focus · HN ↗

                     It&#x27;s a thing you can talk to that does stuff for you. What other &quot;architecture&quot; do you need to know?

                     1. krapp · 1789738775 · focus · HN ↗

                        Fair enough. Your logic is unassailable. There is literally no difference between fiction and reality and no need to understand anything beyond &quot;LLM talk therefore Star Trek real.&quot;

                        1. hannasanarion · 1789742467 · focus · HN ↗

                           Literally not what the comment you were replying to was saying even remotely, but ok.
                  2. actionfromafar · 1789739333 · focus · HN ↗

                     Right. Feel free to extrapolate a reading like &quot;I think LLM tech and a century of tinkering could achieve computer performance similar to what it appears the entirely fictional, voiced by Majel Barrett, Star Trek computers has&quot;.

                     1. krapp · 1789740059 · focus · HN ↗

                        &gt;Feel free to extrapolate a reading like &quot;I think LLM tech and a century of tinkering could achieve computer performance similar to what it appears the entirely fictional, voiced by Majel Barrett, Star Trek computers has&quot;.

                        But that doesn&#x27;t mean anything. &quot;Similar to&quot; is vague enough that it could include video game NPC dialogue.

         3. cindyllm · 1789688818 · focus · HN ↗

            [dead]

         4. corv · 1789690685 · focus · HN ↗

            Bend would make Dijkstra happy even when proof checking can’t verify if the laws are what was actually meant.

            I actually think Asimov is more instructive here, while Gödel and Tarski tell us the tool can’t prove itself…

            Nonetheless, it is a worthwhile endeavor and I hope more rigorous practices like this catch on.

      9. holden_nelson · 1789686608 · focus · HN ↗

         I got the same result when I tried the &quot;remove the walls&quot; example. I followed up by telling it to reimplement up&#x2F;down&#x2F;left&#x2F;right movement without reinserting the walls and it basically made the square with the flag &quot;unenterable&quot;. Like with a force field.

         Respectfully I&#x27;m not sure if I share your worry though. You would have the same problem if you wrote extremely thorough &#x2F; exhaustive unit tests or extremely precise types and didn&#x27;t allow the LLM to amend them. You&#x27;re basically shrinking the state space of what is considered a &quot;correct&quot; program per your spec. That the LLM has to get extremely creative to break your program is a _feature_; in my experience, an LLM does not have to get creative at all to break a typical program written in an enterprise setting, and that&#x27;s unfortunate.

      10. IanCal · 1789723763 · focus · HN ↗

          Side thought - I like the idea of this as a game, where you’re essentially fighting a monkeys paw &#x2F; tricky genie. Not totally sure it’d work but I like the concept of trying not to get caught out.
      11. penguinova · 1789765761 · focus · HN ↗

          [dead]

   7. rao-v · 1789681996 · focus · HN ↗

      Hey Victor! Been following you since HVM&#x2F;Kind, partly because I&#x27;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 &#x2F; cost models to make decisions around SIMD vs. multicore vs. GPU parallelization?

      Bend2&#x27;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!

      1. LightMachine · 1789683316 · focus · HN ↗

         Hi. Yes and of course, I plan to invest in everything that makes Bend better. The language is, in theory, capable of parallelizing perfectly in any setup. Currently, though, only a very simple scheduler is shipped, and you must still tune it manually. We&#x27;re a small team, but we&#x27;re not stopping here, and I hope I can make it grow to the point where that kind of tooling becomes part of the ecosystem.
   8. mathisfun123 · 1789682825 · focus · HN ↗

      what happened to your other project? HVM?

      1. LightMachine · 1789683356 · focus · HN ↗

         Surprise - HVM has been reimplemented in Bend 2.

         You can find it on Bend&#x27;s demo directory in our GitHub.

         Don&#x27;t tell anyone though!

         1. mathisfun123 · 1789683545 · focus · HN ↗

            i&#x27;m asking you what happened to HVM that it needed to be reimplemented as Bend.

            1. LightMachine · 1789685090 · focus · HN ↗

               It didn&#x27;t &quot;need to&quot;, it just evolves by rewrites as I learn (the project is fairly small) so in the latest rewrite I choose Bend!

               1. rowanG077 · 1789744720 · focus · HN ↗

                  That sounds like it&#x27;s dead? The entire point of HVM as I understand was to be an incredibly fast evaluator. If bend2 does not use what right to exist does HVM still have?

                  1. douglasisshiny · 1789745931 · focus · HN ↗

                     &gt;If bend2 does not use what right to exist does HVM still have?

                     What? This is such a weird comment.

                     1. rowanG077 · 1789755596 · focus · HN ↗

                        HVM was too be a highly parallel extremely efficient language target. Bend has taken that place in their ecosystem. I don&#x27;t think that&#x27;s weird question were that leaves HVM.
                  2. LightMachine · 1789761381 · focus · HN ↗

                     no, that&#x27;s a good question. half of the point of HVM is to be an incredibly fast evaluator, in the &quot;raw speed&quot; sense. the other is to be an incredibly fast evaluator, in the &quot;asymptotical&quot; sense. in the first sense, Bend2 supersedes HVM. in the last sense, HVM is still king. on higher order computations that involve λ-calculus and the like, nothing beats the HVM. but I also realize most people aren&#x27;t doing λ-calculations. so, Bend is made for the general public and lower-order programs, while HVM remains for the niche group of researchers and λ-calculus enthusiasts
   9. hei-lima · 1789684763 · focus · HN ↗

      Congrats, Victor!

      É ótimo ver um brasileiro criando algo tão único!

      1. LightMachine · 1789685054 · focus · HN ↗

         obrigado amg
   10. davidw · 1789685698 · focus · HN ↗

       Speaking of lava, you should do a presentation to the local tech group if you&#x27;re ever here in Bend, Oregon...
   11. holden_nelson · 1789686675 · focus · HN ↗

       Just wanted to say this is really, really cool, and impressive stuff. Looking forward to reading your papers and playing with it. Thanks for working hard on it and sharing it with us.
   12. greenlimetea · 1789687917 · focus · HN ↗

       [dead]

   13. pasteleft · 1789701125 · focus · HN ↗

       Thank you for adding a 5-line AGENTS.md. Other projects force you to install skills or MCP even when they&#x27;re just doing the same thing.
   14. didibus · 1789715110 · focus · HN ↗

       Sorry for not knowing, but in the AI world that we are in, I need to learn more about the creator behind a project to trust it. Something that can help me know why the creator is qualified to deliver on the promises being made, that I can trust their judgement and decision, that they know what they are doing and don&#x27;t need AI to tell them what&#x2F;how to do it, and that they are committed long term to the project. Do you think you could share a bit about you that would give me some answers on those?

       1. dgf18 · 1789718302 · focus · HN ↗

          [dead]

       2. killerstorm · 1789721100 · focus · HN ↗

          A lot of information here:

          <a href="https:&#x2F;&#x2F;gist.github.com&#x2F;VictorTaelin&#x2F;77fd5a2a8a4a07e1da6157ebca3c7cf1" rel="nofollow">https:&#x2F;&#x2F;gist.github.com&#x2F;VictorTaelin&#x2F;77fd5a2a8a4a07e1da6157e...

          <a href="https:&#x2F;&#x2F;github.com&#x2F;victortaelin" rel="nofollow">https:&#x2F;&#x2F;github.com&#x2F;victortaelin

   15. IanCal · 1789724552 · focus · HN ↗

       This is a nice reminder for people.

       Cool project!

       This is really interesting, I’ve been very interested in the power of checks for code and things like hypothesis (which seem very similar in terms of writing a “for this kind of case, this holds true”, obviously different in terms of statistical checking vs actual proof).

       I’ll have to explore and this isn’t my field so this isn’t a substantive comment and this may be bikeshedding but I found the game example a little confusing at first because we’d want winning to be possible. It fits the context of stopping a bad thing happening if it’s “evil actor can’t do X” and if your mind is on CTF but games we want to win.

       Potential changes:

       Make it a proof that the game can be won.

       Make it require something first - so the game can’t be won unless the key is found for example. End result is still roughly the same and the failure case is still the same (walk over side of game) but it’s the kind of thing I’d want encoded in a puzzle game - game is winnable, but not winnable without getting the key first.

       Since my other direction normally would be quickcheck style, I’d be interested in cases that are statistically hard to find but easy to prove exist. And in fairness, the other way too I guess. When to use each approach.

       In the spirit of your comment, these are not things I see as failings, they are not things I in any way expect to be changed or done, they are intended as just an outsiders perspective if useful.

       Thanks for making things, and thanks for releasing them!

   16. cyanmoonx · 1789741671 · focus · HN ↗

       [dead]

   17. cyanmoonx · 1789741684 · focus · HN ↗

       [dead]

   18. jsnider3 · 1789744434 · focus · HN ↗

       Glad to see this finally released! What are you doing next?
   19. ycucumber · 1789745718 · focus · HN ↗

       [dead]

   20. tuesdaynight · 1789918986 · focus · HN ↗

       I remember how negative were the comments in your last submission here. They were unnecessary and I never understood why. I hope you get better comments now.

Unofficial Hacker News client; not affiliated with Y Combinator.