How to rewrite mathematics constructively?

If you want a "general method" that "always works" to turn a classical theorem into a constructive one, there are double-negation translations: if you add enough $\neg\neg$s to a classical theorem, you can make a constructively provable statement. However, this rarely produces a constructively meaningful result. Aside from this, there are no fully general methods, but there are general heuristic (and, in some cases, formalizable) techniques and tricks that can be applied.

The most basic technique is learning to recognize when uses of excluded middle, proof by contradiction, and choice are totally unnecessary. This involves inspecting definitions as well as theorems and proofs, looking for occurences of negated statements that can be turned into classically-equivalent positive ones. For instance, if you defined an injective function to be one such that if $x\neq y$ then $f(x)\neq f(y)$, then using that definition is going to involve a lot of excluded middle; but if you remove the unnecessary contrapositive and define it to mean that if $f(x)=f(y)$ then $x=y$, many proofs immediately become more constructive.

Another technique is to replace a negated statement by a classically-equivalent positive one. For instance, if $x$ and $y$ are real numbers, then in constructive analysis we generally replace $x\neq y$ by $x \mathrel{\#} y$ ("$x$ is apart from $y$"), meaning that they are at least some positive rational distance apart. To a certain extent, this can even be formalized: in Linear logic for constructive mathematics I showed that if a proof can be written in a certain variant of affine logic, then it can automatically be interpreted constructively if enough negative statements are replaced by positive ones in this way.

A third technique is to avoid asking for the bare existence of "ideal" objects, such as ultrafilters, prime ideals, zeros of functions, etc. Instead we can replace these by appropriate "approximating systems". For instance, without some form of choice we may not be able to prove that some spectrum has enough points (filters or ideals) to be a nontrivial topological space; but we can instead consider the frame in which those filters would exist as representing a point-free space (locale). Somewhat analogously, without excluded middle we can't prove the usual Intermediate Value Theorem about the actual existence of some zero; but instead we can approximate such a zero by finding a point whose image is as close to zero as desired.

These replacements aren't always classically equivalent. For instance, there are also constructive versions of the intermediate value theorem in which the hypotheses on the function are strengthened, e.g. to say that it never "hovers" around zero. Such strengthenings can often be found by inspecting the proof to see what is "really used" once excluded middle is pared away; often it happens that these stronger hypotheses are satisfied by most practical applications anyway.

These are just a few of the ideas that occur to me; other more dedicated constructivists will probably be able to list many more. Note that a common theme in many of these techniques is to pay attention to computability. Mathematics (even constructive mathematics) always involves idealizations and infinite objects (unless you're a dyed-in-the-wool finitist/predicativist), but certain kinds of "completed infinity" are impossible to compute with, so we can make them more constructive by thinking about how we might represent an approximation computationally, or what actual data would witness the truth of some negative statement.

Finally, regarding Gödel's completeness theorem, as you may know it is equivalent to either weak König's lemma (if the language is countable) or the Boolean Prime Ideal Theorem (if the language is arbitrary). Since these are known to be unprovable constructively, so is the completeness theorem as Gödel stated it. I would say that the version in categorical semantics is the "correct" constructive completeness theorem; sometimes it's unavoidable that a certain amount of nontrivial work is required to turn something into a constructive version (for instance, locales also require some work vis-a-vis topological spaces). This can be regarded as an instance of the general method of "avoiding ideal objects": instead of a single ideal set-model that requires non-constructive principles for its existence, we consider the collection of more concrete categorical models.

Errett Bishop gave some principles in his book on Constructive Analysis:

“The task of making analysis constructive is guided by three basic principles.

• First, to make every concept affirmative. (Even the concept of inequality is affirmative.)
• Second, to avoid definitions that are not relevant. (The concept of a pointwise continuous function is not relevant; a continuous function is one that is uniformly continuous on compact intervals.)
• Third, to avoid pseudogenerality . (Separability hypotheses are freely employed.)”

Those are so openly stated in the founding text of modern constructive mathematics that I don’t think they qualify as tricks. They may not even qualify as helpful advice for a novice, but they are actually reasonable focal points for someone with some experience in the art of constructivizing.

As for the completeness theorem, I never saw a constructive version that I found satisfying, because there is usually no constructive content to the hypothesis that a theory is consistent. But here is a line of thought: What can we do constructively with consistency? Sometimes we have decision procedures. What can we do constructively with a model? Sometimes we build another model. So maybe there is a theorem: If $R$ is a ring with quantifier elimination, then $R[x]/(p)$ also has quantifier elimination. And some version of this for more general algebraic objects could be a distant constructive analog of the completeness theorem....but the line of thought gets so distant so quickly that you might decide that the completeness theorem is not a good place to look for constructivity.

Are you aware that the (semantic) completeness theorem for countable first-order languages is equivalent over RCA0 (a weak subsystem of second-order arithmetic) to WKL0? Essentially the non-constructive part of this lies in the fact that you want to obtain an infinite path from an infinite binary tree. This principle is truly non-constructive, since there is a computable infinite tree with no computable infinite path. So even in the countable realm, which arguably is what truly constructive mathematics should be about, the completeness theorem is non-constructive. But it is not that bad; we can obtain a model of any consistent computable FOL theory that is computable from the first Turing jump.

If you are interested in the use of AC in the uncountable case, the issue lies entirely with whether the theory can be well-ordered. The completeness theorem holds for any theory over a well-orderable language. In general you can find that almost every theorem that invokes AC or Zorn's lemma can be rephrased as theorems about well-ordered stuff whose proofs need no choice. For example, every well-orderable field has an algebraic closure, and every vector space with a well-orderable spanning set has a basis. So even in the usual setting of Zermelo set theory you can easily extract the 'more constructive' version just by adding well-orderability conditions.