While I was reading Dummit and Foote's celebrated Abstract Algebra book, I came across the definition of the polynomial ring $R[x]$ (where, for convenience, they assume that $R$ is a unital commutative ring with $1\ne 0$):
The polynomial ring $R[x]$ in the indeterminate $x$ with coefficients from $R$ is the set of all formal sums $a_n x^n+a_{n-1}x^{n-1}+...+a_1 x+a_0$ with $n\ge 0$ and each $a_i \in R$.
This definition intrigued me because this is the way I am used to seeing polynomials defined in high school textbooks (and I don't think that it is the "correct" way to do it). The part that intrigues me is the following: what is formal about polynomials since we can pretty easily construct $R[x]$? For completeness, I will present below the construction that I am familiar with.
Let $R$ be a nontrivial unital commutative ring (we don't really need it to be commutative; I can't comment on whether we need it to be unital because I have only studied unital rings). Let us denote by $R^{\mathbb{N}}$ the set of sequences $(r_n)_{n\ge 0} \subset R$ of finite support. Without too much trouble we can show that $R^{\mathbb{N}}$ becomes a unital commutative ring with the following operations
$$(r_n)_{n\ge 0}+(s_n)_{n\ge 0}=(r_n+s_n)_{n\ge 0}$$
$$(r_n)_{n\ge 0}(s_n)_{n\ge 0}=(t_n)_{n\ge 0}, \text{where } t_n=\sum_{i+j=n}r_is_j.$$
Then we only need to see that $r \mapsto (r, 0, 0, ...)$ is an injective unital ring homomorphism that allows us to think of $R$ as a subring of $R^{\mathbb{N}}$ (if we don't want to do this identification we may even construct this as a proper inclusion, but this is pretty tedious in my opinion and it is enough if we know that it may be done) and we are basically done if we denote $x:=(0, 1, 0, ...)$: we have obtained our ring $R[x]$.
Now, back to my question. I assume that the formal part consists of the indeterminate $x$ because the definition in Dummit and Foote's book (or in many other textbooks) doesn't really tell us what that indeterminate $x$ is. So, I suppose that if we restrict ourselves to this definition, then polynomials are indeed just some formal sums that magically turn out to have very good properties. But why would one want to do this if we can actually construct the polynomial ring and then there is nothing formal about polynomials? Is it just something done by mathematicians for convenience (because, after all, actually constructing the polynomial ring doesn't help us with anything but the fact that we know that this object can be constructed rigorously)?
Your definition of $R[x]$ is more rigorous, but depending on the student may be harder to intuit. The "formal sums" approach tries to form a bridge between concrete polynomial functions and the more abstract construction $R\leadsto R[x]$. This comes at the cost of some rigor (if we try to untangle what "formal sum" means, we wind up with ... exactly your definition), but may be easier to parse for some students.
Personally, my experience was the opposite: I found the "finite support sequences" definition much more satisfying. But I know that many students in the class I took were confused when the professor laid out that definition, and found the "formal sums" approach more congenial.
(For what it's worth I think we really see an "intuition gap" when we look at multiple indeterminates: the "formal sums" definition of $R[x,y]$ is, I think, likely to be substantially clear than the "two-dimensional array" definition to students new to abstract algebra.)