‹ BackHN Continuity

Thread

Bend – a language that blocks AI mistakes via proof and runs on GPUs

616 points · 327 comments · nicolas-siplis

  1. garrisonj · · focus · HN ↗
    The issue is I’ll have to vibecode all the laws and the laws could be wrong.
    1. drdrey · · focus · HN ↗
      writing specs is hard. For instance the easiest way to comply with "player should never reach the flag" is to disable movement completely, so then you have to specify "player should never reach the flag while still being allowed to move" and so on (liveness). It's not practical for most programs
      1. defmacr0 · · focus · HN ↗
        Yeah, in small examples it's pretty neat: Define a "sorted" property, write a law that checks that the list is sorted and contains the same elements and someone else implements the sort and together with a proof for correctness. However larger software systems have an exponentially larger surface for reasonable and unreasonable edge cases. When I hit ctrl+s in my editor I expect that my cursor does not change colour, that the window does not minimize, that the program does not crash if there is no disk space left and so on. I don't see how this does not devolve into "negative space programming" where the user would have to anticipate and constrain every possible unwanted behavior of his software.
        1. YeGoblynQueenne · · focus · HN ↗
          >> When I hit ctrl+s in my editor I expect that my cursor does not change colour, that the window does not minimize, that the program does not crash if there is no disk space left and so on.

          I take it you haven't used Microsoft Windows?

          Joking, joking...

Open on Hacker News to reply ↗

Unofficial Hacker News client; not affiliated with Y Combinator.