Is Halting Problem is decidable for any real world algorithms? Halting Problem is (theoretically) decidable for such algorithms which termination may be proved in First Order Logic (FOL) because all true statements in FOL are recursively enumerable. It is correct?
I'm talking about programs in Turing-complete languages and use "realworldiness" property not in the sense of finiteness but in the sense of "be designed to some real purpose" and "be not specially cooked to require HOL for termination proof" (that allows potentially to require unprovable statements for termination proof).
As for argument that FOL is adequate for working with ordinary programs is a fact that there are plenty systems designed for industrial application for proving program properties that use only FOL (TLA+, for example).
To be precise, let set of real world programs be all programs that humans write for their utility for entire human history to the end of times.
Perhaps I must say even more precise: Can such property be existing that limits Turing-complete language in such way that termination of any program in language with that property can be proved in FOL but no programmer will be disturbed by that limitation?
And interesting satellite question: is absolutely minimal restriction of Turing-complete languages possible such that Halting Problem become decidable for restricted languages?
 A: FO logic (to be precise, FO[<]) can express no more than star-free languages (McNaughton, Papert, 1971), a proper subset of regular languages. Therefore, I think any hope that FOL is sufficient to express all desired properties programs might have is misguided.
You have to be precise about what the Halting Problem really is and what its undecidability really implies: There can be no algorithm which uniformly decides for any input and any program wether it holds or not.
That does not mean that you can not decide termination for some program, or for (large) sets of programs. In fact, people do that, as exhibited by a recent article in Communications of the ACM.
A: The Halting Problem is solvable for linear bounded automaton, here is a reference.
A linear bounded automaton is a turing machine that has one tape of fixed size that the input is read in on and all computation is performed on it. The basic idea of the algorithm is that since there are only a finite amount of states, all states can be checked to see if they lead to termination. It is very much though a galactic algorithm with a horrible complexity.
On most "real-world" problems there are simpler programs that just look for common mistakes, such as forgotten conditions leading to infinite errors. Of course if you wrote a program looking trying to find a solution to Fermat's Last Theorem's Equation, it would probably say that it will halt (and depending on how much precision you've allowed it just might!). 
