> everything could be formalized in ZFC given sufficient effort

Since I'm not sure what could be comprised under "everything", I don't think I can agree with that statement. The whole point of "practical" formalization efforts is to add some rigor to such assertions. And you've acknowledged that type theoretical foundations can be useful to practitioners, so what's it exactly that you disagree about?