eBPF is a real-world system that also refuses to accept programs that might not halt. You don't have to solve the halting problem, you just have to deny the programmer loops (and loop-alikes, of course; recursive functions, jmp, etc).

IIRC, some language model proved that one-layer of loops can be proven to halt vs not-halt.

As soon as you add a 2nd layer of loops however, you reach Turing-completeness and suddenly the halting problem becomes unsolvable.

-------

So you don't need to deny jmp/loops. You just need to deny _nested_ loops. And... find that old paper I read like 15 years ago to figure out the details to discriminate halt/not-halt in the single-layer loop language.

This is most assuredly false:

    while (state !== STOP):
       read = TAPE[index]
       [state, write, dir] = TABLE[read, state]
       TAPE[index] = write
       index = index + dir

It takes much more. You need to e.g. limit APIs you can call to ones that are also guaranteed to halt, and guarantee an exit condition that is guaranteed to occur, which means either seriously limiting input or adding additional implicit conditions.

E.g. this Ruby program is undecidable:

    gets

This one using a hypothetical gets guaranteed to eventually halt is still undecidable:

    while getsWithTimeout != "halt"
    end

You could ask ChatGPT to find the paper for you! It told me the name of an old videogame I was trying to remember for years.

Microsoft's implementation of eBPF allows for loops :D

https://vbpf.github.io/assets/prevail-paper.pdf

For loops (where the user is not allowed to change the value of the iterator mid-iteration) are guaranteed to terminate.

Or create more loops, since for example adding

For (;;) { print(“hahaha you didn’t say the magic word!”); }

In another loop would also prevent termination without program shutdowns.

Don't let weird C syntax choices fool you, this is a while loop, not a for loop.

To clarify, when I said "for loop", I meant what is sometimes called a "counted for loop" (or simply "counted loop"): there is an (maximum, if you allow early exit) iteration count that is computed before executing the loop and can't increase later.

In C syntax, it is for (int i = 0, e = ...; i < e; ++i) { ... } and the body of the loop is not allowed to change the value of either i or e.

Edit: actually I may have been unclear. When I said "for loops are guaranteed to terminate", in the context of the discussion, I meant "if the only kind of loops you allow are (counted) for loops in a language where loop-free expressions are guaranteed to terminate, you get a language where all expressions are guarantee to terminate". So loops can contain other loops, as long as they are all of the "counted for loop" kind.

Yeah, I just wanted to point out that it's possible in ebpf.

Fair enough :) Although skimming the paper you linked, they say they don't check termination of loops, which surprises me.

Incorrect. The program under inspection could halt or could not halt; undecidability is a statement about Turing machines inspecting that program and unable to make a determination (via a clever proof by contradiction).

The Halting Problem is a truly interesting result, and for the most part uninteresting in practice.

Why is this downvoted? It can't happen that you run an undecidable program, and it halts, since its running would be a proof that it halts.

Say your Turing machine is searching for a contradiction in ZFC. It enumerates all the possible proofs, and checks if they are valid and they prove 0=1. You can prove in ZFC that you can't prove that it halts, nor you can prove that it doesn't halt.

Now your Turing machine won't halt, according to ZFC. (It can halt in practice, if ZFC has a contradiction.) Same for any other undecidable programs.

Problems which cannot be solved by an algorithm/program are considered undecidable as well. Saying that something that doesn't exist, doesn't halts makes no sense in the general case.

The thread is about programs. Existing programs do exist. There are problems not solvable by Turing machines, like the meaning of life, but this thread is not about them.

GGP was talking about programs halting, not halting, and "something else", which GGP called "undecidable".

There are programs that ZFC cannot prove if they halt or not. For example, searching for a contradiction in ZFS is such a program. Its undecidability means that there is no sequence of axioms of ZFC that ends with "this program halts" or "this program does not halt".

But then this program does not halt, since its halting would mean that ZFC can prove that this program halts.

In any case, programs can halt or not halt. There are programs that ZFC cannot prove that they halt or not, but those programs do not halt.

> But then this program does not halt, since its halting would mean that ZFC can prove that this program halts.

That step is not logically consistent. It could halt, it's just that ZFC can't prove it will ever do so. For example, the program which computes the 8000th busy beaver number halts (per definition of the busy beaver function), but is undecidable in ZFC[1].

An undecidable program can halt. An undecidable program can run forever. But whatever axiom system is being used to decide that can't prove which (without running the program, potentially for an infinite number of steps).

[1] https://scottaaronson.blog/?p=2725

> For example, the program which computes the 8000th busy beaver number

I don't believe that there exist such a program.

Why not? That implies that an 8000 state Turing machine which eventually halts when started with a blank tape doesn't exist. If any of them do (and it's trivial to simulate one), then exactly such a program can exist.

Well, there can indeed exist a program that writes out the number BB(8000). (In the sense that it is consistent with ZFC that there is a program that writes out the number of steps of the smallest contradiction in ZFC.)

What I don't believe that there exist a program that is a proper counter-example, that is, its halting is undecidable in ZFC, and it halts. Exactly because what I wrote earlier.

Actually, this comment makes sense and is used in logic to derive true but non-provable propositions withing the current axiom system assuming it is sound.

The problem is that you dont know if the checker that you use to detect if a program halts will itself halt on your given input or continue forever. But given a sound checker with some assumption, one can find non-halting programs which wont be detected by the checker using the diagonalization trick.

n = 1;

while (isFamousMathProblemWeDontKnowWhetherItHoldsForAllTheIntegers(n)) { n++ }