Crowding the boundary of non-constructivity without crossing it? Can any sense be made out of my vague feeling that some proofs in Ramsey theory are as close as you can get to non-constructive proofs without crossing the line?  Is there any way to make this precise?
PS: OK, the short version of the elaboration of which I wrote in the comments below goes like this: In many areas of mathematics, if you want to prove that $X$ exists, you somehow figure out some plausible guess about which object $X$ is or where to find $X$, and then you work on figuring out how to rigorously prove that $X$ is it.  In Ramsey theory, it seems as if you have a systematically eliminate every suspect one-by-one and until nothing else is left but $X$.
Alright, one concrete example: Shortly before posting this I had worked through this elementary exercise: In a set of $(n-1)m+1$ people, show that either there is a set of $m$ who are mutually unacquainted or there is one who knows at least $n$ others.
I came up with a description of an algorithm, as follows.
$(1)$ Initially let $A=\varnothing$.  We will increment $A$ by adding a new member to it as many times as this algorithm occasions that addition.  The members of the set $A$ will always be mutually unacquainted.
$(2)$ Does some member of $A$ know at least $n$ non-members of $A$?  If so, STOP.  We're done.
$(3)$ Otherwise, each member of $A$ knows at most $n-1$ non-members of $A$, so the total number of people known by members of $A$ is at most $(n-1)|A|\le(n-1)m<(n-1)m+1$.  In that case, at least one non-member of $A$ is unknown to all members of $A$.  Let the new value of $A$ be $A\cup\{\text{that one non-member of $A$}\}$.
$(4)$ If $|A|=m$ the STOP; we're done.  Otherwise return to $(2)$ and go on from there.
 A: One reason for this phenomenon is that the finite version of Ramsey's theorem, in the end, relies on the pigeonhole principle for the base case of an inductive argument. (Indeed, one reasonable way to understand Ramsey's theorem is that it is just a stronger statement of the pigeonhole principle). Because the natural algorithm that realizes the pigeonhole principle is a brute-force search, algorithms for the general case take on the same character.
For a concrete example, suppose that we have just 2 colors and are coloring singletons, and want a homogeneous set of size 100. We know that it is enough to color 199 elements, but given 199 elements, the only straightforward way to find a homogeneous set of size 100 is to look through the elements until we find 100 of the same color. There is no structure in the problem that we can try to exploit, just 199 elements each of which has one of two colors.
Nevertheless, of course, a brute force search over a finite set looking for elements with a decidable property is perfectly constructive, when we know already that the search will succeed.
In the full Ramsey theorem, where we color $[\mathbb{N}]^k$ with $l$ colors and want an infinite homogeneous set, aspects of the computability of the pigeonhole principle turn out to be very relevant.
The pigeonhole principle states that if $\mathbb{N} = C_1 \cup C_2$, then at least one of $C_1$ and $C_2$ is infinite. Now, if we have a computable 2-coloring of $\mathbb{N}$, there will be a computable solution to that instance of Ramsey's theorem: either $C_1$ or $C_2$. But there is no way to determine, just given algorithms for $C_1$ and $C_2$, which of them will be infinite, as a function of the algorithms. Thus we would say that the proof of Ramsey's theorem for exponent 1 is "effective", but not "uniform".
This becomes important when we look at exponent $2$. Now we have a coloring $f$ of $[\mathbb{N}]^2$ and we want an infinite set $H$ with $[H]^2$ monochromatic. One common proof starts with this construction: for each $n \in \mathbb{N}$, induce a coloring $f_n$ of $\{n+1, n+2, \ldots\}$ via the rule $f_n(m) = f(n,m)$.  Each of these functions $f_n$ must have an infinite monochromatic set, by induction. 
But, even if $f$ is computable, we may not be able to tell as a function of $n$ whether $f_n$ has an infinite monochromatic set of color 1, or whether it has one of color 2. That nonuniformity in the proof of the pigeonhole principle becomes an obstacle to an effective proof of Ramsey's theorem for 2 colors and exponent 2. In fact, the computability of Ramsey's theorem has been very well explored, and in particular we know that there are computable 2-colorings of $[\mathbb{N}]^2$ with no computable infinite monochromatic set.  The finite case, while perfectly constructive, reflects some of the nonconstructivity of the general Ramsey's theorem. 
A: Comment was too short.
My intuition is that a proof is constructive if it gives an algorithm which constructs some representation of the desired object (the algorithm here has a slightly broader meaning than the usual notion in computer science). However, that algorithm might be infeasible/intracable, i.e. the number of operations it requires may make it unusable even for small inputs (e.g. see this class). 
In such case we know the algorithm exists, but it doesn't help us in constructing the object. Strangely we find ourselves in situation that is practically (whatever that would mean in this abstract setting) no better than one with non-constructive proof. I would say that this is very close to your boundary and Ramsey theory does involve numbers so huge that my imagination has problems handling them.
I'm not sure if this is more precise than your description, but nevertheless I hope it helps $\ddot\smile$
