We've hit the comment depth limit, so I'll reply here. > it's not clear to me why you necessarily want the language you use to rigorously investigate the found

We've hit the comment depth limit, so I'll reply here. > it's not clear to me why you necessarily want the language you use to rigorously investigate the foundations of mathematics to be the same one you use to do proof verification. Among other things, I want theorems about foundations to be useful to non-foundational mathematicians. Working on type theory can improve, at the very least, formal verification tools. In my view, traditional ZFC-based mathematical logic has a much smaller likelihood of being useful for regular mathematicians. For example, the vast majority of mathematicians will never explicitly assume the existence of a large cardinal in a paper. It seems to me that the difference in usefulness is probably due to their relative distance from common discourse.