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]:

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/ https://xkcd.com/1266/