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

Unofficial Hacker News client; not affiliated with Y Combinator.