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?