There are many different views of formalization for mathematics. They are not all competing in the same scope. There are different degrees of formalization. Three analogies for this are
spectrum of formalization, from informal (e.g., Latex) to increasing formality, like CAS and then to Proof assistants.
"levels of zoom" as in visualization, like Google Maps but for Math
compiling "high level concepts" (e.g., Latex) to controlled natural language to proofs
The idea of "zooming visualization" is relevant to the user experience -- a reader should be able to select the level of granularity.
The idea of "compiling" is about making implicit concepts explicit. Also, compiling to different architectures is similar to formalizing in different logics and axioms. Unlike the visualization concept, there is not one underlying basis to specify formalization in.