When does (or should) Theoretical CS care about intuitionistic proofs?
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.