I agree with this but want to stress something else.
A really great formal language actually frees you from "every detail, no matter how obvious". That's the heart of abstraction.
Good mathematics is heavily abstracted because it forms a superhighway between mathematical concepts that allows you to lift and transport intuition from one context to another without forsaking formality.
To some degree these abstractions must always be built from nitty gritty details. In mathematics it's a matter of didactics to find the most efficient bootstrapping process. In computer science it's a matter of library and language design.
Abstraction works only with strong context. A few symbols in an equation are a miracle of conciseness, but meaningful only after the symbols, operators and formal system are defined.
I never claimed otherwise. I think in fact that there are two forms of context—didactic and mandatory.
Didactic context is personal, the context required for or used by a particular person in order to conceptualize and build confidence with a set of concepts (and their associated syntax, though it's close to meaningless so long as it doesn't get in your way too much).
Mandatory context is more like a compact notion of why and how some mechanism is applied. For instance, you might bootstrap homology using point-set topology (educational context) and then enhance it using algebraic topology. Eventually, perhaps, the mandatory context is that homology is a measure of non-exactness of chain complexes and this concept can be lifted from its base context and presented wherever exactness is an interesting measure.
Point being—language hardly exists in a vacuum. Good language invokes powerful concepts in an efficient manner and allows you to construct arguments using them. Good arguments can link seemingly disparate concepts with ease.
A really great formal language actually frees you from "every detail, no matter how obvious". That's the heart of abstraction.
Good mathematics is heavily abstracted because it forms a superhighway between mathematical concepts that allows you to lift and transport intuition from one context to another without forsaking formality.
To some degree these abstractions must always be built from nitty gritty details. In mathematics it's a matter of didactics to find the most efficient bootstrapping process. In computer science it's a matter of library and language design.