Modern math textbooks are based on naïve set theory, which can be quite feasibly modeled, even by structural foundations. It might require some effort at the lowest layer of formalization, but even then only as a one-time thing that's not going to impact the project as a whole.
That may very well be the case, but to a person starting out right now, those foundations seem to be lacking right now (or at least are not easily discoverable).
