Halting problem only stops you from your prover from working on all programs.

On some programs like "stop" or "while(true)" the proof is easy.

With more sophisticated analysers it becomes possible on wider range of programs.