Good for you. I also think pure maths can be a fun diversion.
> The fact that they have any bearing on the real world is a mildly interesting diversion.
Well, computer "science" is primarily an engineering discipline. It is therefore primarily, if not entirely, about having bearing on the real world. (And even if it were a "science", which it largely isn't, that would still be the case).
> Given this frame of reference, empirical evidence almost never enters the picture when justifying a proof.
Given this frame of reference, your proof is of no relevance to software, which was exactly my point: yes, you can do these proofs, but they are largely irrelevant, and even if relevant always subsidiary to empirical evidence.
> Indeed, empirical evidence is necessarily finite, whilst even some of the most simple proofs reference the infinite.
How do you know that while these proofs reference the infinite, they are actually applicable to the infinite? The answer is: you don't and you can't. You can only assume that the proof mechanisms you use actually do not break down. Now I am certainly convinced (= I believe) that induction will continue to work for all N if I prove 1 and N -> N+1, but I have only empirical evidence for small N to justify that belief. And if we found an M where it didn't, what then?
And of course, there always have been (and probably always will be) "proofs" that were later shown not to be correct, just like physical "laws" that turned out not to be laws. All knowledge is contingent, especially all-quantified knowledge.
And I have to admit that I find the naive/rigid belief (it is no more than that) in the absolute power of proofs...charming :-)
I would say that software engineering was the engineering discipline, and computer science a mathematical discipline.
My point was that the proof itself is not subsidiary to empirical evidence, only its application is, and in my eyes, there is merit in the proof, free from its application to the "real world", for example as a lemma to another proof. Consider it a form of separation of concerns: whilst I prove a theorem, I am not concerned with how it mirrors the observable world, but in order to apply it, of course I must ensure that its assumptions can be reliably observed. In this way, our "beliefs" are limited and do not taint the logic of the proof itself.
> How do you know that while these proofs reference the infinite, they are actually applicable to the infinite?
Which brings us to your next point: I do not know, I simply believe it to be true because it is convenient to do so. My point is that this belief or its refutation does not affect the worthiness of the proof, only that of its application.
I actually do not believe in the absolute power of proof, I don't think it is something you can get away with believing once presented with all the facts. I hope I've explained myself better in this comment though: I don't think our views are as antipodal as it first seemed.