When people say that Appel-Haken did not really contribute understanding, they aren't necessarily talking about the four-color problem itself. They mean that the proof did not really contribute any understanding of mathematics.
A famous example when the proof of a long-standing conjecture really did contribute a lot of understanding is Andrew Wiles' proof of Fermat's Last Theorem. People weren't excited about this proof because they cared directly about the answer to FLT; they were excited because the proof brought together and integrated ideas from many disciplines and represented progress on the much larger Langlands program. Similarly, Perelman's proof of the Poincare Conjecture introduced important new ideas and tools. This was why many experts were convinced that Perelman's proof was valid even before it was formally checked; the high-level summary contained enough nontrivial ideas that they already saw that there was something extremely interesting going on.
In other words, the problem with Appel-Haken is that it is boring. It was more or less an application of an already-understood technique, just on a larger scale, and so has led to very little interesting new mathematics. People are still looking for a conceptual proof of the Four-Color Theorem analogous to the two proofs above, for example people working in quantum topology; see this blog post by Noah Snyder and Kainen's Quantum interpretations of the four-color theorem. A proof along these lines would be much more interesting, as it would likely shed light on a number of other issues in quantum topology.
This principle applies to more than just long-standing open problems. Many problems you might encounter in an undergraduate course might be solvable by a tedious computation along the lines of the Appel-Haken proof, but often there exist much more interesting conceptual proofs along the lines of Wiles' proof. If you stopped after finding the tedious calculation you might never find the conceptual argument, which often turns out to be much more interesting (e.g. it naturally suggests generalizations, interesting concepts, ties to other branches of mathematics...).
I will take your comment about quadratic equations as an example. It's true that the quadratic formula allows you to solve quadratic equations mechanistically. The question, then, is whether the quadratic formula leads to any significant conceptual understanding of polynomials. For example, does it suggest a natural route to the cubic formula?
If you think of the quadratic equation in terms of completing the square, then you quickly run into a problem: you cannot, in general, complete the cube. So completing the square does not generalize to cubic equations. If you want to understand cubic equations, it follows that you need to think about the quadratic formula more conceptually.
The conceptual breakthrough is the following: what the quadratic formula really shows you is that there is a symmetry to the roots of a quadratic polynomial. The roots
$$x_1 = \frac{-b + \sqrt{b^2 - 4ac}}{2a}$$
and
$$x_2 = \frac{-b - \sqrt{b^2 - 4ac}}{2a}$$
are conjugate: they are related by a symmetry which flips the sign of the square root. This symmetry manifests itself concretely in the fact that the sum
$$x_1 + x_2 = - \frac{b}{a}$$
is completely invariant under flipping the sign of the square root, whereas the sum
$$x_1 - x_2 = \frac{ \sqrt{b^2 - 4ac} }{a}$$
is completely negated under flipping the sign of the square root. Taking this idea seriously leads you to the method of Lagrange resolvents, and now if you were born in the right century you would be well on your way to inventing group theory, Galois theory, and (if you were really observant) representation theory.
Isn't that way more interesting than using the quadratic formula?
Kempe's "proof" used induction on the number of vertices in the graph G. Given a graph with n vertices, he removed a vertex, colored the remaining graph in four colors using the inductive hypothesis, and then (and this is the hard part) re-inserted the missing vertex, which possibly resulted in having to "fix up" the coloring of its adjacent vertices - this is where the problem occurred.
The Heawood counterexample showed very clearly why the algorithm that Kempe used was invalid - when applied to Heawood's graph, it did not have the intended result. Thus it was this algorithmic portion of the proof that had a logical error that was exposed by the Heawood counterexample.
There are quite a few expositions of this entire affair; one chosen more or less at random is at
http://web.stonehill.edu/compsci/LC/Four-Color/Four-color.htm
Best Answer
This is a possible coloring. Done by hand, either really lucky or not that difficult. Perhaps it'll help with debug of the algorithm and shows that this map is definitely legal.