[jkrejcha]

Adding on (and it's not terribly relevant to eBPF), it's also worth noting that there are trivial programs you can prove DON'T halt.

A trivial example[1]:

    int main() {
        while (true) {}
        int x = foo();
        return x;
    }

This program trivially runs forever[2], and indeed many static code analyzers will point out that everything after the `while (true) {}` line is unreachable.

I feel like the halting problem is incredibly widely misunderstood to be similar to be about "ANY program" when it really talks about "ALL programs".

[1]: In C++, this is undefined behavior technically, but C and most other programming languages define the behavior of this (or equivalent) function.

[2]: Fun relevant xkcd: https://xkcd.com/1266/

[fwip]

EDIT: I am incorrect, please ignore. (Original text below, for posterity).

Nit: In many languages, doesn't this depend on what foo() does? e.g:

  foo() {
    exit(0);
  }

[loeg]

No? The foo() invocation is never reached because the while loop never terminates.

[fwip]

Apologies; I misread the function call as being inside the loop.