‹ 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. dylanowen · · focus · HN ↗
      100% agree. It's crazy so many Ai articles are heralding the end of code while at the same time defining more complex ways to write code under a different name.
      1. Neywiny · · focus · HN ↗
        I suppose I could look it up but I wonder if people thought this of "high level" languages like C when it first came out. No more assembly. Or even assembly instead of machine code.
    2. NohatCoder · · focus · HN ↗
      This is the age old problem with proving correctness. You can (sometimes) prove that two programs have identical behaviour. One of the programs can be slightly simpler in that it is only concerned with what the correct result of a given operation is, not how to get there. But this doesn't fundamentally change that the complete specification is almost as complicated as the program itself.
    3. misja111 · · focus · HN ↗
      Exactly. You could simplify things by giving AI a limited set of laws, but then you'd risk that AI would make some mistake in the parts that you didn't cover. So a failsafe set of laws would look very much like an actual program.
    4. 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.