HST is usually proven through the existence of a unique minimum-norm vector in a nonempty closed convex set. I think this is an existential proof which applies to infinite dimensional spaces.
However, to actually apply the result in a real world problem, one might need to find the actual numeric value of the minimum-norm vector through construction. Furthermore, constructivism is appreciated in mathematical economics and operation research mathematics.
Do we have a simple constructive proof for HST over $\mathbb R^n$ or a linear space?