When I'm constructing a nonstandard model by by adding in a new constant symbol and invoking compactness, it feels much more like I'm adding in $c$ and "closing under Skolem functions" (at least symbolically) rather than recursively adding in new witnesses to existential statements, even though these seem like just two different descriptions of the same process.
I'm curious if there are any fiddly details in formalizing this approach. Are there any sources that describe this step of the Henkin construction in this way? How does one formalize this approach?
Let me point out that Henkin constants are just $0$-ary Skolem functions.
Given a formula $\varphi(x,y_1,\dots,y_n)$, a Skolem function for $\varphi$ is an $n$-ary function $f_\varphi$ such that $$\forall y_1,\dots,y_n\,(\exists x\, \varphi(x,y_1,\dots,y_n)\rightarrow \varphi(f(y_1,\dots,y_n),y_1,\dots,y_n)).$$
In the special case $n = 0$, we get a $0$-ary function symbol, i.e. a constant symbol $c_\varphi$, such that $$\exists x\, \varphi(x)\rightarrow \varphi(c_\varphi),$$ which is exactly a Henkin constant.
One interesting thing about the Henkin construction is that we can get away with only introducing $0$-ary Skolem functions, instead of fully Skolemizing. The reason is that in the model produced by the construction, every element is named by a constant symbol. So if we want a witness for the existential formula with parameters $\exists x\, \varphi(x,b_1,\dots,b_n)$, instead of applying a Skolem function $f_\varphi(b_1,\dots,b_n)$, we can instead find constants $c_1,\dots,c_n$ whose interpretations are $b_1,\dots,b_n$, and then use the Henkin constant for the sentence $\exists x\,\varphi(x,c_1,\dots,c_n)$.
If you're using a Henkin construction to prove the compactness theorem (as is done e.g. in Marker or Hodges), then you're free to go all the way to Skolemization. This won't make the proof any harder, because it's easy to show that if you take a finitely satisfiable theory $T$ and Skolemize, the result is still finitely satisfiable (since any model of a finite chunk of $T$ can be expanded by Skolem functions).
On the other hand, if you're using a Henkin construction to prove the completeness theorem, I think there's a real benefit to using Henkin constants instead of Skolem functions. The key step is proving that if $T$ is a consistent theory (i.e. it doesn't prove $\bot$), then the Henkinization/Skolemization of $T$ is still consistent. In this step, we have to think about the details of how our proof system works, and it's more convenient if we only have to deal with the axioms for Henkin constants, rather than the more complicated axioms for Skolem functions.