Precise definition of free group

Sure, you can make this totally precise. There is no reason to assume $S$ is countable; just let $S$ be any set. Let $T=S\times\{0,1\}$; we think of elements of the form $(s,0)\in T$ as representing "$s$" and $(s,1)$ as representing "$s^{-1}$". Write $\pi_0:T\to S$ for the projection map onto the first coordinate and $\pi_1:T\to \{0,1\}$ for the projection map onto the second coordinate. If $n\in\mathbb{N}$, write $[n]=\{i\in\mathbb{N}:i<n\}$ and say that a word (on $T$) of length $n$ is a function $w:[n]\to T$. Say that a word $w$ is reduced if for all $i<n-1$, if $\pi_0(w(i))=\pi_0(w(i+1))$ then $\pi_1(w(i))=\pi_1(w(i+1))$ (intuitively, this means that your word never has $s$ adjacent to $s^{-1}$). Given a word $w:[n]\to T$, say that another word $w':[n-2]\to T$ is a one-step reduction of $w$ if there exists $i<n-1$ such that $\pi_0(w(i))=\pi_0(w(i+1))$, $\pi_1(w(i))\neq \pi_1(w(i+1))$, and $w'$ is given by the formula $$w'(j)=\begin{cases} w(j) & \text{ if $j<i$} \\ w(j+2) & \text{ if $j\geq i$.}\end{cases}$$ (Intuitively, you are obtaining $w'$ from $w$ by cancelling an adjacent $s$ and $s^{-1}$ appearing in the word $w$).

Write $W$ for the set of all words on $T$ (of any length). Say that a word $w'$ is a reduction of a word $w$ if there exists a natural number $n$ and function $v:[n]\to W$ such that $v(0)=w$, $v(n-1)=w'$, and $v(i+1)$ is a one-step reduction of $v(i)$ for each $i<n-1$. It is then possible to prove the following theorem:

Theorem: Let $w\in W$. Then there is a unique reduced word that is a reduction of $w$.

The proof is a bit messy but not too hard, and uses induction on the length of $w$. Write $r(w)$ for the unique reduced word that is a reduction of $w$.

We need one more ingredient before we can define the free group. Given two words $w:[n]\to T$ and $w':[m]\to T$, define their concatenation $w*w':[n+m]\to T$ by the formula $$(w*w')(i)=\begin{cases} w(i) & \text{ if $i<n$} \\ w'(i-n) & \text{ if $i\geq n$.}\end{cases}$$

We can now define the free group. Let $F(S)$ (the "free group on $S$") be the set of all reduced words on $T$, and define a multiplication $\cdot:F(S)\times F(S)\to F(S)$ by $w\cdot w'=r(w*w')$, i.e. the reduced word obtained by reducing the concatenation of $w$ and $w'$. You can then prove that $(F(S),\cdot)$ is a group.

There are a few ways to think of a free group. Certainly one of them is the construction from words you noted in your post.

Another is linked to in the comments: The free group on a set S satisfies a "universal property". Namely there is an inclusion $$i: S \to F_S$$ where F is the free group on S, such that if $$g: S \to G$$ is any homomorphism there is a unique homomorphism $$\phi: F_S \to G$$ such that $\phi \circ i = g$.

I would definitely consider this to be the "precise" way to define a free group in the language of category theory.

Another way which I think to be intuitive, but less precise, is to think of groups in terms of generators and relations. Every group can be written in terms of a generating set and relations between those elements. A free group is simply a group which has generators but no relations between them.

In fact if S is a generating set for G, then the kernel of the homomorphism $\phi$ from before is generated by the relations of G.

In my opinion, precise definition of a free group should be based on the concepts word, sub-word, empty word, inverse word, cancelation, reduced word, and juxtaposition. These concepts are easy to grasp and is really clear and precise. Even if you define a free group in terms of category theory (functors and homomorphism), known as a universal property, you would want to apply to the notions of words and generators in order to prove the existence of a free group. Of course, there may be purely categorical proof of existence of a free group (like here), but it is not simpler than usual proof using words and generators. This is a good resource explaining this approach.
Another reason for giving a definition of a free group in terms of words and generators is that it is easier to grasp for computer scientists who usually deal with strings, algorithms or rewrite systems.