Right--this will work on some types of side-channel attacks. For example, I could prove that my decryption function runs in a constant amount of time no matter

Right--this will work on some types of side-channel attacks. For example, I could prove that my decryption function runs in a constant amount of time no matter the input. However, you can't proactively defend against side-channel attacks. By definition, a side-channel attack exists because the designer didn't know that the cryptosystem leaks information when (s)he designed and proved the correctness of the implementation. Proving that the cryptosystem doesn't leak information is damn nigh impossible, and often outside the scope of software engineering. My favorite example is acoustic analysis (https://www.cs.tau.ac.il/~tromer/acoustic/ https://www.cs.tau.ac.il/~tromer/acoustic/). Before this was shown to be possible, how were cryptosystem designers supposed to know to defend against it? The best we can do is come up with and formalize a threat model, and then prove that the cryptosystem is secure against the adversaries in the threat model. The problem is that threat models don't help you with adversaries in the future, who have means of getting information from your cryptosystem that you didn't think of.