> We really don't have a good terminology for distinguishing between efficient constructive proofs (those corresponding to efficient algorithms) and inefficient

> We really don't have a good terminology for distinguishing between efficient constructive proofs (those corresponding to efficient algorithms) and inefficient ones... We do: the complexity classes P and NP. Ok, technically this is a polynomial time decidable language (does there exist etc. etc.), so perhaps consider FP and FNP (the function variants of P & NP).