Thread

1. lutusp · 1789728576 · 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. zamadatix · 1789745662 · focus · HN ↗

      Graybeards in computer science sometimes need to remember the halting problem only states you cannot make a general algorithm which answers the halting question for all possible program+input pairs. Importantly, it does not state it's impossible to make an algorithm which can check if the given program+possible inputs will halt (or even if a given subset of all possible programs will - e.g., trivially, finitely long ones not given a means of recursion or allowed infinitely long inputs).

      Separately, the halting problem would not apply in the first place. The claim and goal is only to approve programs for which the given proof can be shown to work and then accept it when it does, not to guarantee every possible bend program and condition set will be able to have a working proof. Practically, this means if the proofing mechanism can not do that in the time+space bounds the solver is given then thats just treated as a rejection of the given proof (regardless whether the proposed program does or does not actually fit the requirements) and the LLM is back at trying to create a program which is feasibly provable.

      1. lutusp · 1789749163 · focus · HN ↗

         > Separately, the halting problem would not apply in the first place.

         The halting problem applies to all systems able to perform Peano arithmetic. Therefore it applies to all non-trivial programs -- the program being tested, the program performing the test, and the program verifying the result.

         > The claim and goal is only to approve programs for which the given proof can be shown to work and then accept it when it does ...

         Yes, but that's not what's being claimed. My objection was to the original claim, not this restatement.

         > ... and the LLM is back at trying to create a program which is feasibly provable.

         No non-trivial computer program is "feasibly provable." That's what the Halting Problem makes impossible.

         1. skew · 1789842604 · focus · HN ↗

            > The halting problem applies to all systems able to perform Peano arithmetic.

            You're confusing the halting problem with Gödel's first incompleteness theorem.

            And Bend is just claiming to be sound but incomplete

            1. lutusp · 1789921011 · focus · HN ↗

               > You're confusing the halting problem with Gödel's first incompleteness theorem.

               So did Alan Turing, but ... he wasn't confused. The two are connected.

               > And Bend is just claiming to be sound but incomplete

               That is not what was said. Here it is:

               "Bend – a language that blocks AI mistakes via proof."

               That's not possible, and changing what was claimed is not productive.

Unofficial Hacker News client; not affiliated with Y Combinator.