‹ BackHN Continuity

Thread

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

616 points · 327 comments · nicolas-siplis

  1. lutusp · · focus · HN ↗
    Beginners in computer science need to understand that there's no such thing as a computer programming method or discipline that "blocks AI mistakes via proof." This is not a position or opinion, it is a fundamental constraint called the "Halting Problem," originally identified by Alan Turing in 1936.

    What applies to computer programming also applies to AI, for a reason that should be obvious. Lean, a widely used theorem prover, its everyday description notwithstanding, is Turing-complete and is therefore subject to the Halting Problem as well.

    This is not meant to disparage one person's project. It is meant to identify a limit that applies to all such projects.

    1. skew · · focus · HN ↗
      You are the one being insufficiently precise here. There would only be fundamental obstacles if there was an additional claim "allows all correct programs".

      The Halting problem states only that is no computable function that takes another P program as input and always terminates with a correct answer of whether P halts. It's certainly possible to write a program that always terminates with an answer of either HALTS or UNKNOWN, and only says HALT when that's true, it's just that it will also return UNKNOWN for some (or all) programs that do actually halt.

      1. lutusp · · focus · HN ↗
        > It's certainly possible to write a program that always terminates with an answer of either HALTS or UNKNOWN, and only says HALT when that's true, it's just that it will also return UNKNOWN for some (or all) programs that do actually halt.

        Any program running in a Turing-complete environment is subject to the Halting Problem. So, given that constraint, your example program cannot be relied on to do any specific thing. That's the meaning of the Turing Halting Problem.

        <a href="https:&#x2F;&#x2F;en.wikipedia.org&#x2F;wiki&#x2F;Halting_problem" rel="nofollow">https:&#x2F;&#x2F;en.wikipedia.org&#x2F;wiki&#x2F;Halting_problem : &quot;Alan Turing proved in 1937 that the halting problem is undecidable, meaning that no general algorithm exists that can correctly solve the problem for all possible program–input pairs.&quot;

        Focus your attention on the word &quot;undecidable&quot;.

Open on Hacker News to reply ↗

Unofficial Hacker News client; not affiliated with Y Combinator.