I think you can reason it like this.

Assuming certain constraints (what you can define bounded analysis rules for) you can prove that things terminate. These rules things are usually far more advanced than we suspect initially, but they're not still not fully unbounded.(And we can often come up with more rules to make things practical even if unwieldy)

Deciding termination for an arbitrarily large program in a turing complete system CAN require no less than execution of such a program thus we CANNOT guarantee to be able to verify termination for EVERY program. (This is the halting problem)

I spent a lot of time on my thesis learning about type inference systems and as many such systems for uncooperative languages(JS,Python,etc) need to do abstract interpretation they fall into the same kind of issues and this is why practical systems use JIT compilation instead of AOT even if there are exceptions (Shed Skin Python is quite impressive for example).

I thought any general system contain arithmetic (as the proof based on transformation) cannot be proved it will be halted. Termination ... can it be terminated without halting?

Halting is indeed the same as termination. The halting problem DOES allow you to prove that some programs terminate. The problem is that there will be other programs that do terminate, but you won't be able to prove that they terminate.

So there is no way to know, for EVERY possible program, whether that program will terminate or not. But there are still some programs that you can know for certain that those programs will terminate.