Formal definition of effective proof I am someone who likes precise definitions for mathematical terminology. So, is there some text where there is a precise definition of an effective proof? The notion is vague to me.
 A: There is no single formal definition of an "effective proof", just as there is no single formal definition of a "constructive proof". 
It is known is that, if the existence of a mathematical object is provable from particular axiom systems, then the object itself must be computable. This is clearest when the object is of a type to which "computable" easily applies: a set of natural numbers, a function from natural numbers to natural numbers, etc.
One such axiom system, using classical logic, is the system of second-order arithmetic known as $\mathsf{RCA}_0$. Because this system has a model in which every object is computable, any object that the theory proves to exist must be computable. There are systems that have similar properties but use non-classical intuitionistic logic.
In non-classical logic, another way of getting computable witnesses for existential statements is the method of realizability; this is closely related to the BHK interpretation of constructive mathematics. There are systems for which each provable statement has a computable realizer, and these realizers give computable witnesses.
Also closely related are the fields of computable analysis (which, by convention, uses classical logic) and constructive analysis (which, by convention, will use intuitionistic logic). These areas are directly concerned with proofs for which the constructed objects are computable or constructive in various senses.
A: A strickly formal definition of an axiomatic proof:
A proof of a theorem is a list of formulas where:
1) Each formula is 
1a) an axiom or
1b) can be deducted from one or more earlier formulas in the list by a given inference rule.
and 
2) the theorem to proof is the last formula in the list.
Notice that hardly any proof is given this way.
