I don't think it needs to be so dramatic. You could have a proof that the algorithms don't contain data-dependent logic, and perhaps ensure that no data-dependent instructions are generated; and that all branches have the same number of instrution-cycles (adding padding if not). You'd then simply rely on the architecture-specific instruction timing differences to be respected by the compiler.

Would something like this guarantee that no side-channels are possible on any architecture? Perhaps not, but it would still get you most of the way there.