You can use mathematics to prove other things as well. You could e.g. use a special bool type for all secure data that you can't branch on, so that no secrets could be exposed by examining the runtime path of execution. Or build a model of your CPU's caching and prefetching behaviour and prove that you're code doesn't expose any secrets by that channel.
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/). 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.
I take your point, but I don't think _anything_ can defend against unknown attacks. However, we could defend against all known attacks using formal methods, which is a lot better than we're doing at the moment. Further, when a new attack becomes known, I would wager that having something that is verifiable today will be easier to verify or fix in the future, as compared to a code-base that is not provable.
Just because we can't achieve theoretical perfection, we should not rule out using methods that would solve many of the actual problems we encounter today.
Of course, if you can find a way to defend against unknown future problems, I'm all in favor of using your method!
But the ideas of trusted OS and instruction might be necessary to compartment secrets to reduce their potential exposure to the least possible opportunity. It's basically impossible to completely eliminate plaintext and secrets in clear unless maths allow it, but we should still try.
