Formalization is often presented (1) as a further stage after axiomatization. (It is often said that euclidian geometry was already axiomatized, but not yet formalized ( or not enough), and that the complete formalization of geometry was only achieved much later, by Tarsky for example) (2) it is is also presented as the full completion of axiomatization.
Reference : " if geometry is to be deductive, the deduction must everywhere be independant of the meaning of geometrical concepts , just as it must be independant of the diagrams; only the relations specified in the propositions and definitions employed may legitimately be taken into account" Pasch ( quoted by Wilder, Introduction To The Foundations Of Mathematics, Part I The axiomatic method, I, §1 Evolution of the method. )
My question is : why is this further stage needed? why formalizing mathematics? ( what is the interest in ordinary mathematical practice? why should a fully axiomatized mathematical theory be also formalized?)
Remark.- My question is not equivalent to " is the formalist view of mathematics correct?" I'm looking for an answer mathematicians could agree on , whatever might be their own commitment to a particular philosophy of mathematics?