Essential vs. non-essential uses of proof-by-contradiction

Preliminary remark: I'm just a working mathematician, not a logician.

It often happens that we are faced with a useful implication ${\cal A}\Rightarrow{\cal B}$, but the contraposition $\neg{\cal B}\>\Rightarrow\>\neg{\cal A}$ is easier to prove. Such a proof should not be called a "proof by contradiction".

An example: You are given an equilateral triangle $\triangle$ of side length $2$ and a bag full of equilateral triangles of side length $a<2$. Then the following useful fact is true: If you can cover $\triangle$ with five small triangles then you can cover $\triangle$ with four small triangles.

It is hopeless to get an overview over all coverings with five small triangles and to produce for each of them a covering using only four triangles. But the contraposition, "If you cannot do it with four you cannot do it with five", has a one-line proof which I won't reveal here.

But there are statements of type ${\cal A}$, which really have to be proven by adding the axiom $\neg{\cal A}$ to mathematics and deriving a contradiction. A well known example is the statement that $\sqrt{2}$ is irrational (but even in this case some wise guy might find a way out).

The most common class of logics that don't support proof by contradiction are intuitionistic or constructive logics. (I'll use "constructive" and "intuitionistic" more or less interchangeably here.) Specifically, this means that they don't support any of the following equivalent statements (or any other equivalent statement): the Law of Excluded Middle ($P\lor\neg P$), Double Negation Elimination ($\neg\neg P\implies P$), Peirce's Law ($((P\implies Q)\implies P)\implies P$), Contraposition ($(\neg Q\implies \neg P)\implies (P\implies Q)$).

Proof by contradiction corresponds to a slight variant of Double Negation Elimination. Namely, even intuitionistically $\neg P \equiv (P\implies \bot)$. (In fact, this is often true by definition in intuitionistic systems.) Proof by contradiction is then $(\neg P \implies \bot)\implies P$. This is not to be conflated with reductio ad absurdum which is $(P\implies \bot)\implies\neg P$ which is valid intuitionistically. (Again, often by definition.) Notice how we can't use reductio ad absurdum to get proof by contradiction by simply instantiating it with $\neg P$; that just gives us $(\neg P \implies \bot)\implies \neg\neg P$. We'd still need Double Negation Elimination to get $P$.

It's extremely common to conflate the above rules so it is often unclear which people mean when they say "proof by contradiction" or "reductio ad absurdum". I make the choice I do because reductio ad absurdum (as I've defined it) doesn't prove something, it refutes it, while proof by contradiction does prove something. When I want to be clear though, I usually call use Double Negation Elimination for proof by contradiction and $\neg$ introduction for reductio ad absurdum as $\neg$ introduction is unambiguous (but this terminology is usually not familiar to those who haven't studied a bit of [structural] proof theory).

Terminology out of the way and to answer your actual questions, theorems that can be proven constructively (i.e. in constructive or intuitionistic logic) don't "essentially" require proof by contradiction, even if there is a proof that does use it. Theorems that aren't true in intuitionistic logic do "essentially" require proof by contradiction (assuming they are true classically). If we interpret "true" as "not refutable", then we can embed classical logic into intuitionistic logic. This process is mechanical and not only does it allow us to mechanically translate classically provable theorems into intuitionistically provable theorems, but it also mechanically translates classical proofs into intuitionistic proofs. Of course, the theorems are "weaker" on the intuitionistic side, e.g. Double Negation Elimination would be translated to $\neg\neg P \implies \neg\neg P$ by these translations.

Theoretically, constructive proofs can be no easier than classical proofs since a constructive proof is a classical proof. In practice, many classical proofs are constructive and restricting oneself to a constructive proof limits the search space a bit (and makes it a bit better structured). It's pretty easy to argue that classical principles like Double Negation Elimination are non-intuitive, and I will touch on that in a bit. However, a constructive proof, in general, contains a lot more information than a classical proof. The term "constructive" comes from the idea that a proof should provide a means to "construct" a "witness". A constructive proof corresponds to an algorithm for actually constructing a witness to a statement. This is most dramatic for existential statements. To constructively prove an existential statement means you have to actually build the thing that is claimed to exist. This can be a lot more work (and even impossible) than merely claiming something exists without providing any means (and there may be no means) of creating the thing that supposedly exists as many classical proofs do. On the other hand, explicit constructions are often highly informative, and a significant part of the content of a theorem may actually be the explicit construction used in the proof. (For example, I'm reading "Computational Complexity: A Modern Approach". The famous Cook-Levin theorem that proves that SAT is NP-complete is proven by encoding the execution of a Turing machine as a (polynomial-sized) Boolean formula. This construction can then be used to prove that a problem is in P if and only if there is a polynomial-sized logspace-uniform family of circuits that solve the problem. It's not at all obvious why SAT being NP-complete would imply this, but from the proof of Cook-Levin it's not that hard to see.)

So constructive proofs can require (potentially much) more work than classical proofs not "just" because they are working in a weaker system (which is itself very highly valuable as many more interesting things are models of intuitionistic logic than classical logic), but also such proofs are more informative. Another way to see the difference in work is to look at the computational interpretation of these systems. The Curry-Howard correspondence famously shows that propositions, proofs, and proof transformations correspond to types, programs, and program transformations. The most specific interpretation of "Curry-Howard correspondence", which at this point is often taken more like a principle, is the specific result that the Natural Deduction presentation of Intuitionistic Propositional Logic corresponds to the Simply Typed Lambda Calculus. More recently, a similar correspondence has been found for classical logics. The notable thing here is that classical principles correspond to control operators like call/cc. Indeed, the type of call/cc is $((A\to B)\to A)\to A)$ which looks exactly like Peirce's Law! These are (in)famously expressive but difficult to understand (just like proof by contradiction). This means that using call/cc can result in much shorter programs, but call/cc itself is difficult to understand and it complicates the understanding of every part of the program, even parts that don't themselves use call/cc. The embedding of classical logic into intuitionistic logic I mentioned earlier corresponds to Continuation-Passing Style (CPS) which is a method often used to understand and implement control operators. Here's an interactive description in story form that illustrates what actually happens with the Law of Excluded Middle computationally (modulo artistic license, but see the referenced paper by Phil Wadler for the original story [which I prefer] and the less colorfully presented details).

As a final note, there's a difference between a specific theorem being proven constructively and working in a constructive logic. We can have a constructive proof that manipulates non-constructively provable statements. This corresponds to writing a program that has access to subroutines that are not themselves implementable (often this is called an oracle). Working within constructive logic generally requires a decent amount of reworking of various definitions. For example, constructively various classically equivalent formulations of "finite" become constructively inequivalent, and so it matters how you specify that a set is "finite". Similarly, the usual formulation of the Intermediate Value Theorem is not true constructively, but a suitably similar statement can be proven (within the context of a constructive formulation of real numbers). At this point large swathes of mathematics have been redone in constructive frameworks. However, even within a classical framework, there is a lot of value to constructive proofs, and there is a lot of value to knowing which results are constructively provable.