Proving termination for programs written in models less powerful than a Turing machine does not require you to solve the halting problem. Programs using primitive recursion, finite automata, and regular expressions, for example, can all be proved to terminate, and can express a number of useful computations.
The problem is that the pickle module is far too permissive. In particular, the REDUCE operation invokes a Python callable with an argument tuple on the pickle stack, which means that 'pickles' are at least as powerful (in the Turing-general, halting problem sense) as Python.