Ok, total agreement there. I think denotations are pretty identical to languages in the sense that you pick one you like then defend it to the death but, should

Ok, total agreement there. I think denotations are pretty identical to languages in the sense that you pick one you like then defend it to the death but, should you choose, could always learn to use more and would profit massively from doing so. 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.