Everything I am writing below is carried out explicitly in Chapter III of Silverman's book on elliptic curves. In the earlier chapters, he defines the Picard group.
For any curve over any field, algebraic geometers are interested in an associated group called the Picard group. It is a certain quotient of the free abelian group on points of the curve. It consists of formal sums of points on the curve modulo those formal sums that come from looking at the zeroes and poles of some rational functionfunctions. It is a very important tool in the study of algebraic curves.
The very special thing about elliptic curves, as opposed to other curves, is that they turn out to have a be in natural set-theoretic bijection with their own Picard groups (or actually, the subgroup $Pic^0(E)$). The bijection is as follows: let O be the point at infinity. Then send a point P on the elliptic curve to the formal sum of points [P] - [O]. (It is not obvious that this is a bijection, but the work to prove it is all "pure geometric reasoning" with no computations.) So there is automatically a group law on the points of E. Then it requires no messy formulas to show that under this group law, the sum of three collinear points is O. So for free, you also get that this group law is the same as the one you defined in the question and that the one you defined is associative!
