"computation" absolutely did arise from noticing how the merely formal could faithfully adhere and correspond to the concrete. So it is "grounded" in that sense. There continue to be arguments of how best to ground the formalities.
See, that is the gist. 1 + 1 = 2 is formal. Not merely formal, actually formal. It requires the student to understand and own a formal system. The set of integers and the additive operation. So what we are really talking about here is what actually occurs when a student takes ownership of a formal system. What difference does it make if one apple and one apple always makes two apples in the real world if 1 + 1 isn't always 2 in the student's head, all by itself? Over time, that formal system grows and becomes more involved and more self sustaining.
When you say "how to best ground the formalities" what you really mean is how to reach students unaware of the formalities, but the formalities themselves are grounded in one thing only, formal thinking (is that better than "reasoned thought"?). If you fail with the formalities then you have failed period and you fail with the formalities when you have failed to invoke formal thinking in the student.
You said that the "mapping" between formal thinking and the real world is important. How so? I spend hours, days, and even weeks pondering some problems with nary a single thought of the real world. But I agree, when we apply mathematics to the real world, that mapping is very important. But this is irrelevant to my claim. If you have not developed formal thinking then any notion of mapping is moot, is it not? The real issue that I am concerned with here is what role does common sense, namely concrete examples, play in the development of formal thinking. After searching deep, the only role I can come up with is as an aid in communicating the basic properties of the formal system you are trying to teach and as a tangible check against which you test the formal reasoning you are developing. I gave examples of things (coordinate transformations etc.) that are entirely of formal origin and I could fill page after page of similar examples. This tells me that formal reasoning, once developed, is entirely grounded in its own domain, separate of the real world.