I like your phrase "transport understanding"; an important part of programming is dealing with informal understandings of what the software does or is intended to do. Most programming has very little formal reasoning in.
So there are holy wars to be expected.
I think you point out something really interesting with this notion of formal/informal. I think it's tough to draw that line because a lot of "formal" reasoning is designed to be informally used but needs formality in its presentation.
Or, to be more concrete, I think that most programmers use a slew of semi-actualized denotations when understanding code. Usually this is a transparent process and a skill gained by experienced programmers is to align your semi-actualized denotations so that they both agree with one another and with reality.
Formalism is just a tool to get ahold of these and fully actualize them. It's something one could choose to invest in—or not.
But the underlying process of transporting understanding and using the best denotation for the moment is very real regardless of the level of formality.
The formal term of note here is "denotation" in that "a language may be understood through its denotation" as an abstract machine or as a mathematical object. The best understanding comes from recognizing that many denotations may be valid for a language and that great richness comes from this. To work, the denotations must be in alignment in various ways and when they are it means that you can transport understanding from one denotation to another to the language itself.
So I don't think there's an honest conflict, though I imagine there are programmers and PL experts who either (a) honestly only ever use one denotation or (b) play favorites and this may lead to some clouding of things.