I am not ignoring any of that. Nothing says that you can't work with non-constructive logic in a programming language, or analyze non-constructive logics
as programming languages. In fact that can be extremely useful although it's also, at present, difficult and not super common.
The things you listed are extremely close to one of the foundational fields of CS, namely programming language theory. It's funny that you should bring up the law of the excluded middle because I learned a lot about it by studying PL theory: did you know that adding callCC to your typed lambda calculus turns it from a constructive logic system to a classical one? And that double negation translation is just a CPS transform which, at least for me, is a heck of a lot easier to reason about than proof theory directly?
Everything in math is, at least in theory, provable. Provable in a discrete system (ie a formal logic) even if it's reasoning about something that isn't discrete. So there's nothing fundamental stopping us from doing exactly the same proofs in a formal system that a computer can understand. Oh, say, a programming language.
Of course, with current technology, it's difficult from a practical standpoint, but there's nothing fundamental stopping us. And ideally it's something we should do to ward off errors and also to create proof artifacts that can be analyzed and manipulated systematically.
Wouldn't static analysis for mathematical proofs be great? Or papers written as libraries so that relying on a lemma literally links against the proof it was first defined in.
Seriously, if you dive into PL theory you'll see that the line separating CS from math doesn't really exist except as a social and technological phenomenon. (Lots of things are fundamentally possible but too difficult to do in reality, at least right now.)