Summary
Ok so I agree with some of the answers but I think people are underestimating how rigorous and conservative compilers are in their transformations and optimisations. Long story short - although optimal code generation is indeed a sort of black art and 99% of the time heuristics are used rather than proofs (someone talked about the Denali super optimiser) correct code generation is, in fact, mathematically sound and it is designed to be so. The fact that there are bugs is due to the enormous complexity of compiler codebases. As a side node, an automatic theorem prover can have bugs, even though every part of it is mathematically sound, so the fact that compilers have bugs doesn't mean they are random collections of rewrite rules.
Now, to answer your questions in turn:
How does a compiler programmer know when it's OK to interchange loops?
There is a subfield of compiler theory called Dependence Analysis that deals with questions like that. There are entire books on the topic, but for your particular question: the compiler will automatically figure out the iteration space of the loop (if the bounds are computable, see NB at the bottom), it will figure out dependencies between the instructions of the loops (there are different kinds of dependencies), it will compute the distance and direction vectors of the loop, and then figure out if it's legal to do the interchange. The Wikipedia article on this just gives the different types of dependencies but has links to other subtopics, and also cites the book I mentioned.
And, in general, do they use mathematical proofs to demonstrate conclusions?
No, not in general. Also depends on what we mean by proof - do you mean using a theorem prover? The Denali paper uses a SAT solver, for example. The Dafny compiler and language, by Microsoft Research @ Cambridge, bakes in verification of your code by virtue of source level language annotations. The compiler verifies the correctness of your code, although to work with annotations is very difficult (I've fiddled with Dafny for a project at university and I speak from experience). Also, by "not in general" I mean not in gcc, the llvm family and I would suspect (but I haven't checked) in the Intel's icc. And again, we are talking here about C-like source to machine level compilation, nothing fancier.
How does a compiler programmer know that their compiler will generate correct code? How do they test their conclusion? Do they have to write a test suite that runs the compiler, and checks that the generated code is correct?
The other answers covered this extensively so there's not much more to say. I guess I can add that since compilers are really BEASTS in terms of complexity, testing them extensively is paramount. Also, I would like to reiterate that even in a mathematically sound piece of code (if we assume we have such notions formally defined) there could be bugs in the infrastructure that handles that code, so testing is always important.
Verdict
Compilers are very complicated. They need to be fast to enable seamless edit-compile-debug developer loops, and also correct. Compilers' correctness of the code they produce is kind of "locally mathematically sound" - every transformation that the compiler does must preserve the semantics of the original program. Improvements in speed are driven by heuristical algorithms, and such algorithms are good examples of black art techniques in the sense that they give no proof that the resulting code will be faster. They also give no formal proof that it will be correct, but every transformation is designed to produce correct semantic preserving code. Finally, the hottest trend in compilers (I guess as everywhere else in Computer Science these days) is to use machine learning for optimisations, so we'll have even more knobs to tune :) yay
NB
Almost everything in the compiler "back end" i.e. the codegenerator, is either NP complete or undecidable. In particular, to determine if loop interchange is legal is undecidable, since loop bounds can be arbitrary expressions (say function calls). However, if the bounds are computable (say integers or something simple) then that's where Dependence Analysis kicks in.
