As I said in the comments, intuitionist logic is not the main point. The more important point is having a constructive proof. I think Martin-Löf's type theory is much more relevant to programming language theory than intuitionistic logic and there are experts who have argued that Martin-Löf's work is the main reason for the revival of the general interest in constructive mathematics.
The computability interpretation of constructiveness is one possible perspective, but it is not the only one. We should be careful here when we want to compare constructive proofs to classical proofs. Although both might use the same symbols, what they mean by those symbols are different.
It is always good to remember that classical proofs can be translated to intuitionistic proofs. In other words, in a sense, classical logic is a subsystem of intuitionistic logic. Therefore you can realize (say using computable functions) classical proofs in a sense. On the other hand, we can think of constructive mathematics as some mathematical system in classical setting.
At the end, formalisms, whether classical or constructive, are tools for us to express statements. Taking a classical theorem and trying to prove it constructively without this perspective doesn't make much sense IMHO. When I say $A \lor B$ classically I mean something different from what I say $A \lor B$ constructively. You can argue what "should" be the real meaning of "$\lor$" but I think that is not interesting if we are not discussing what we want to express in the first place. Do we mean (at least) one of them holds and we know which one? Or do we simply mean one of them holds?
Now, with this perspective, if we want to prove a statement like $\forall x \ \exists y \ \varphi(x,y)$ and we want to relate this to a mapping from $x$ to some $y$ satisfying $\varphi(x,y)$ then the better way to express can be the constructive way. On the other hand, if we only care about the existence of $y$ and do not care about how to find them then the classical way would probably make more sense. When you prove the statement constructively, you are also implicitly building an algorithm for finding $y$ from $x$. You can do the same thing explicitly with a more complicate formula like "the algorithm $A$ has the property that for all $x$, $\varphi(x,A(x))$" where $A$ is some explicitly given algorithm.
If it is not clear why one may prefer the constructive way to express this, think about programming languages as an analogy: you can write a program for the Kruskal's MST algorithm in x86 assembly language where you have to care about lots of side issues or you can write a program in Python.
Now why we don't use intuitionist logic in practice? There are several reasons. For example, most of us are not trained with that mind setting. Also finding a classical proof of a statement might be much easier than finding a constructive proof of it. Or we might care about low-level details which are hidden and not accessible in a constructive setting (see also linear logic). Or we might simply be uninterested in getting the extra stuff that comes with a constructive proof. And although there are tools to extract programs from proofs these tools generally need very detailed proofs and haven't been user-friendly enough for the general theorist. In short, too much pain for too little benefit.
Here is one possible reason why we don't see much constructive proofs in theory A:
our theorems in theory A are often $\Pi^0_2$ statements and are proven using not very strong theories (say they are provable in $PA$) and by a meta-theorem all of them are also provable constructively (in the constructive counterpart of $PA$). In fact, many theory A results can be proven in theories much weaker than $PA$.
I remember that Douglas S. Bridges in the introduction to his computability theory book argued that we should prove our results constructively. He gives an example which IIRC is essentially as follows:
Assume that you work for a big software company and your manager asks you for a program to solve a problem. Would it be acceptable to return with two programs and tell your manager one of these two solves correctly but I don't know which one?
At end, we should keep in mind that although we use the same symbols for classical and intuitionistic logics these symbols have different meanings, and the one to use depends on what we want to express.
For your last question, I think Robertson–Seymour theorem would be an example of a theorem that we know it is true classically but we don't have any constructive proof of it. See also