‹ BackHN Continuity

Thread

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

616 points · 327 comments · nicolas-siplis

  1. runeks · · focus · HN ↗
    > In the post-AGI economy, humans will eventually stop writing and reading code, but we still need an ambiguity-free way to tell the AIs building the world around us what we want done.

    > With laws, our intents can be much more precise than natural language.

    Doesn't this just mean that the code is now "laws", ie. the code is now the spec.

    Given this, is there any reason think that writing the "laws" for a complex system is any easier than writing the old-fashioned code that implements it?

    1. sidharthkmenon · · focus · HN ↗
      Yeah i think empirically you've hit the nail on the head (and there are some ties here to computability theory, e.g. Rice's thm).

      sometimes the specification is easier to write than the code (sorting algo vs. quicksort impl) and sometimes the spec is much harder (what's "a good user experience"? what does "high availability" in a distributed system mean, precisely?)

      i think it's just not true that it's easy to formally verify everything, it's often much easier to just write the code lol (e.g. sel4 is 200k+ lines of proof, ~50k lines of code iirc).

Open on Hacker News to reply ↗

Unofficial Hacker News client; not affiliated with Y Combinator.