I think the most surprising thing I've learned taking formal math in college is just how much mathematicians are pragmatists (at least for my teacher with sample size n=1). They're much more interested in new ways to think about ideas, with a side effect of proofs for correctness. The proof is more about explaining why something works, not that it does.

I'm going to take a formal logic class in the fall, and my professor said something akin to "definitely take it if you're interested, just be aware that it probably won't come in use in most of the mathematics done today." The thing is the foundations are mostly laid, and people are interested in using said foundations for interesting things, not for constantly revisiting the foundations.

I think this is one reason most mathematicians don't see a need for formal proof assistants, since from their perspective it's one very small part of math, and not the interesting one.

This is not to say that proof assistants are a dead end—I find them fascinating and hope they continue to grow—but there's a reason that they haven't had a ton of traction.

I think that's a good way of putting it. I would addend that most people working in mathematics aren't generalists, their primary interest isn't in a broad picture. Rather, most are hyperfocused into a single domain with a strong backbone of reflexive intuition built up. By virtue of sheer human limitation, there's only so much someone can care about what's happening outside of their world while still making serious contributions within it. This doesn't even just extend all the way to shifting foundations, but number theorists can hardly be expected to keep up with the forefront of graph theory, for example.

For the pragmatists Logic as a field commits the immortal sin: it blasphemes the intuition that mathematicians spend years honing by obliterating it. Not just for a singular domain, but for all domains. Of course, that doesn't really explain the whole picture. Formalism built a holy walled city. Logicians, by nature of their work, leave the safety of the walled city to survey, exploit and die in the tangled jungle outside. Some don't even speak the holy language of the glorious walled city, they talk in absolutely gibberish modalities and hyperstructures. There is a political tension held against logic and logicians as a result.