[YeGoblynQueenne]

>> As a general matter, you can't prove a predicate true or false by automatic means.

Not in the general case, sure, yet in practice I'm sure we've all written plenty of code that terminates just fine. [Edit: I'm talking about imperative as well as logic or functional programming code].

The question then is- what does it mean when a program terminates? In the case of principled approaches like logic or functional programming, you have a pretty good idea what that means (e.g. a logic program proves a theory true or false). When an imperative program terminates, it's a very hairy affair to say what, exactly, termination means.

[Edit 2: Actually, if you think about it, there's nothing we can really achieve in the general case (including machine learning; see language learning in the limit). In practice, on the other hand, we're doing things, alright - by continuously relaxing principles and fudging limits as necessary (see PAC learning)].