In this talk, I argue in favor of stepwise formalization where depending on need and expertise, different stages of formalization or automation can lead to different useful results. I illustrate how this has affected the MathLang project. The MathLang project aims at computerizing mathematical texts in a way that puts priority on the needs of the working mathematician and the ordinary reader of mathematics, instead of the more usual approach of making things easier for the mathematical logician. MathLang allows (but does not require) recording more of the semantic structure of a mathematical text than typesetting systems like LaTeX and semantic web formats like OpenMath and OMDoc. MathLang avoids requiring any commitment to a particular logical framework or foundation of mathematics (e.g., set theory, category theory, type theory, etc.) or to a particular software system for checking, finding, or building proofs (e.g., Coq, Isabelle, Mizar, etc.). MathLang avoids requiring full formalization, because full formalization is extremely expensive (in salaries), but at the same time MathLang provides support for moving toward full formalization in stages that can be divided between different workers. MathLang's design is divided into _aspects_ that handle different parts of the structure of a mathematical text. One aspect deals with the basic grammar of mathematical statements (the mathematical uses of terms, nouns, adjectives, statements, etc.) and checking of basic well-formedness issues (such as defining things before using them). Another aspect handles the connection between the grammar and the natural language phrases and mathematical formula that visually represent mathematical statements. Another aspect deals with larger issues of document structure and inter-document dependencies. Further aspects being developed handle connections with formal foundations of mathematics and give support for completing formal proofs. I will discuss the progress so far in the MathLang project as well as future directions.