Explicit algorithms and algorithms involving unknowns Let's assume the you have two algorithms for computing some single but complicated number (e.g., the Ramsey number $R(5,5)$). Both are provided as high-level, semi-formal textbook descriptions.


*

*The first algorithm, by means of some textual reformatting and filling in the usual gaps in high-level reasoning, can be easily (say, within several days of coding) turned into a (relatively large) computer program in some imperative programming language, including that of Turing machines (provided appropriate tooling support, of course).

*The second algorithm can almost be turned into code in some imperative programming language, except there are some unknown constants (e.g., the algorithm contains an assignment "$x := c^2$", where $c$ is nonconstructively defined by Theorem 5.19.38, which says $\exists\,c\in \mathbb{N}\colon\dots$). In the best case, this algorithm has some merits such as creating a connection to some other area of mathematics, and in the worst case, this algorithm is simply "'print $r$;', where $r$ is the constant $R(5,5)$". We know that the second algorithm solves our task, i.e., that a Turing machine corresponding to our high-level description exists, but we don't know some part of this algorithm exactly.
In mathematical writing, how do you call these algorithms when you provide the reader with them? I mean, how do you distinguish between them? Do you say explicit/nonexplicit? Effective/noneffective? Any other pair of terms?
 A: 1.   This would be called a constructive proof. Quoting from the linked wikipedia page:

In mathematics, a constructive proof is a method of proof that demonstrates the existence of a mathematical object by creating or providing a method for creating the object. This is in contrast to a non-constructive proof (also known as an existence proof or pure existence theorem) which proves the existence of a particular kind of object without providing an example.

2.   This would be called an existential (or existence) proof:

An existence theorem is purely theoretical if the proof given of it does not also indicate a construction of the kind of object whose existence is asserted. Such a proof is non-constructive, and the point is that the whole approach may not lend itself to construction. In terms of algorithms, purely theoretical existence theorems bypass all algorithms for finding what is asserted to exist. They contrast with "constructive" existence theorems.

Most algorithms are constructive, but not all. From Non-constructive algorithm existence proofs, which also gives a few examples of the latter:

The vast majority of positive results about computational problems are constructive proofs [...] However, there are several non-constructive results, where an algorithm is proved to exist without showing the algorithm itself.

