When does (or should) Theoretical CS care about intuitionistic proofs? From what I understand (which is very little, so please correct me where I err!), theory of programming languages is often concerned with "intuitionistic" proofs. In my own interpretation, the approach requires us to take seriously the consequences of computation on logic and provability. A proof cannot exist unless there exists an algorithm constructing the consequences from the hypotheses. We might reject as an axiom the principle of the excluded middle, for instance, because it exhibits some object, which is either $X$ or $\lnot X$, nonconstructively.

The above philosophy might lead us to prefer intuitionistically valid proofs over ones that are not. However, I have not seen any concern about actually using intuitionistic logic in papers in other areas of theoretical CS. We seem happy to prove our results using classical logic. For example, one might imagine using the principle of the excluded middle to prove that an algorithm is correct. In other words, we care about and take seriously a computationally-limited universe in our results, but not necessarily in our proofs of these results.

1. Are researchers in theoretical CS ever concerned about writing intuitionistically valid proofs? I could easily imagine a subfield of theoretical computer science that seeks to understand when TCS results, especially algorithmic ones, hold in intuitionistic logic (or more interestingly, when they don't). But I have not yet come across any.

2. Is there any philosophical argument that they should? It seems like one could claim that computer science results ought to be proven intuitionistically when possible, and we ought to know which results require e.g. PEM. Has anyone tried to make such an argument? Or perhaps there is a consensus that this question is just not very important?

3. As a side question, I am curious to know examples of cases where this actually matters: Are there important TCS results known to hold in classical logic but not in intuitionistic logic? Or suspected not to hold in intuitionistic logic. 

Apologies for the softness of the question! It may require rewording or reinterpretation after hearing from the experts.
It is is worth thinking about WHY intuistionistic logic is the natural logic for computation, since all too often people get lost in the technical details and fail to grasp the essence of the issue.

Very simply, classical logic is a logic of perfect information: all statements within the system are assumed to be known or knowable as unambiguously true or false.

Intuistionistic logic, on the other hand, has room for statements with unknown and unknowable truth values.  This is essential for computation, since, thanks to the undecidability of termination in the general case, it will not always be certain what the truth value of some statements will be, or even whether or not a truth value can ever be assigned to certain statements.

Beyond this, it turns out that even in strongly normalizing environments, where termination is always guaranteed, classical logic is still problematic, since double negation elimination $\neg\neg P \implies P$ ultimately boils down to being able to pull a value "out of thin air" rather than directly computing it.

In my opinion, these "semantic" reasons are a much more important motivation for the use of  intuistionistic logic for computation than any other technical reasons one could marshal.