Right, the halting problem means one can hardly prove anything at all when it comes to software.

Sure buddy. And the uncertainty principle means you can't prove I was at the scene of the crime.

The fact phones don't usually wipe themselves will be plenty good for a judge.

Btw: Regardless of the above I support this guy's right to protect his private data from baseless and unreasonable searches. He should not be charged with a crime.

No, it means there is no general solution to the problem of proving software correct. You can prove if a specific program will halt or not given certain parameters. You cannot write an algorithm that will work to prove if any arbitrary program will halt.