I think the point is that even though one can't determine loop termination for all loops (easily provable), there are a huge number of useful loops that do useful work and for which you can prove properties like termination (and other static properties).
> there are a huge number of useful loops that do useful work and for which you can prove properties like termination
Exactly! If the loop doesn't terminate, then you obviously cannot show it. But if it does, then you should be able to (even if that requires some changes to help the tool)
> If the loop doesn't terminate, then you obviously cannot show it.
I don't think this is true for all loops either - some can be proven to never terminate, just like some can be proven to terminate. And some can't be proven either way.
Assuming you meant 'busy_bever' to implement the busy beaver function, said function is in fact not a computable function, which means you can't write it down in a programming language.
This is true but somewhat misleading. The nth busy beaver numbers are known for n <= 4. It's within the bounds of possibility that we will some day learn the nth busy beaver numbers for n <= 10. (What we can say is that the parent's loop will never terminate for any known definition of "ever" that pertains to the physical universe.)
That's not a very good exemple because with BB we know the code terminates, by definition. The canonical tong-in-cheek argument is to use the Collatz conjoncture instead (but even that isn't a good example in practice: https://news.ycombinator.com/item?id=21440306)
But that's not something these kinds of tools are supposed do, even with trivial functions… These tools have no idea about the run-time (and there's no way they coule, since it depends on the load you put on the hardware in parallel of running your program)
I agree. There are tools though which are specifically for determining worst-case execution time for e.g. embedded systems which can actually give accurate timing information (upto a point).
Yeah, so these tools will not tell you how long it will take to terminate --- only that it will eventually. In the vast majority of cases, that is what you want to know.
I remember there was a theorem that one can find an arbitrary substring in a long enough output of infinite (stationary) random process. I also suppose that a decimal representation of pi may count as one, then your function provably terminates.
But this is of a theoretic interest. In practice the verifier says: "I can't prove that this function will terminate within (some reasonable window), program rejected". And this is what's actually needed: a program that provably has certain properties, where an automatic proof is tractable.
It is currently not known whether π is a normal number (that is, its representation in any base contains any finite sequence of digits with the same density as in a uniformly random string of digits).
I think the point is that even though one can't determine loop termination for all loops (easily provable), there are a huge number of useful loops that do useful work and for which you can prove properties like termination (and other static properties).