What can we gain by losing infinity?

I think you're conflating opinions about when math is useful with opinions on the nature of math itself. Formalism does not assume that "all rules are equally valid". You can be a staunch formalist and yet still believe that X set of axioms are the only useful ones and everyone who assumes different axioms is wasting their time. You could be a formalist and still believe that the concept of infinity is leading math astray from useful math. Many of the differences you lay out seem to just be in people's opinion on which axioms are useful and which aren't. That's still formalism.

Setting that aside, it's very difficult for me to take non-formalist views of mathematics seriously. I strongly suspect that anyone who subscribes to those views has some deep-seated confusion in their heads.

> Platonism, which believes [mathematical objects] exist in some timeless realm beyond this physical universe

This is equivalent to formalism, except perhaps in how the mathematician feels about it. What could any possible difference be? In what way could it ever matter in the slightest whether something "really exists", if we define that to be so weak as to include "in some timeless realm beyond this universe"? Surely pink goblins "really exist" in this sense as well. With such a weak definition, the difference between your "really exists" and my "really exists" is purely emotional.

> Yet another view is conceptualism-mathematical objects really exist, but in the human mind.

You can be formalist and still argue about whether humans invented or discovered math. Beyond that, this is again just relying on the weakest possible definition of "really exists", with some added human-centric arrogance added in. Crows can count to 5; it's patently absurd to claim they are using something that is "not mathematics" or some completely alien form of mathematics that humans cannot access, because it's crow-brain math rather than human-brain math. This sounds like the Copenhangen Interpretation but for math: humans brains are magic! What are we doing? What are we talking about?

> This idea that some mathematical objects are in a philosophical sense “more real” than others is a big motivator of mathematical constructivism

Yet again, this is still formalism. Up until here, you've used the word "real" in such a weak tautological sense as to have no connection to our (or any possible) universe. But here, you've switched back to "real" meaning "having any bearing on our universe". So you're saying "constructivists consider different axioms useful than ZFC mathematicians do." More often they don't even really think about usefuless at all, it's just something that caught their interest and they decided to explore it.

There simply is no "non-formalist" mathematics.

> I think you're conflating opinions about when math is useful with opinions on the nature of math itself. Formalism does not assume that "all rules are equally valid"

I think you're misinterpreting what I was saying. Of course, a formalist will say that some rules are "more valid" in the sense that they produce more interesting or useful theorems. My point was, to a formalist, there is nothing more to be said about the validity of axioms than the value of the theorems they produce. Whereas, from certain other perspectives in the philosophy of mathematics, that is not the only grounds on which axioms can be judged.

> This is equivalent to formalism, except perhaps in how the mathematician feels about it. What could any possible difference be? In what way could it ever matter in the slightest whether something "really exists", if we define that to be so weak as to include "in some timeless realm beyond this universe"? Surely pink goblins "really exist" in this sense as well. With such a weak definition, the difference between your "really exists" and my "really exists" is purely emotional.

You sound like a logical positivist. And that's the issue – if your philosophical assumptions are positivist, then non-positivist philosophies of mathematics (and of anything else) simply aren't going to be intelligible to you. They can only make sense if you are at least willing to doubt for a moment your positivist assumptions.

> Crows can count to 5; it's patently absurd to claim they are using something that is "not mathematics" or some completely alien form of mathematics that humans cannot access, because it's crow-brain math rather than human-brain math. This sounds like the Copenhangen Interpretation but for math: humans brains are magic! What are we doing? What are we talking about?

Conceptualism claims that mathematics exists in the mind–but it doesn't claim necessarily only human minds. If animals have minds too, then mathematics can exist in animal minds as well, even if in a much more rudimentary form. I doubt any conceptualist would say, that if intelligent extraterrestrial life were discovered to exist, that their minds wouldn't contain mathematics simply because they are a different species from homo sapiens.

> So you're saying "constructivists consider different axioms useful than ZFC mathematicians do." More often they don't even really think about usefuless at all, it's just something that caught their interest and they decided to explore it.

There are different types of constructivists: (a) those who have a philosophical commitment to constructivism; (b) those who are interested in constructivism for practical reasons (related to computer science); (c) those who are just interested in it as an interesting mathematical system to explore. You can be (b) or (c) without needing any philosophical commitments at all, and they are completely compatible with a formalist philosophy of mathematics. And, quite possibly, the majority working in constructive mathematics today are (b) or (c) not (a). But, historically, the founders of constructive mathematics (e.g. Brouwer) were very much (a) not (b) or (c).

> There simply is no "non-formalist" mathematics.

I think you are conflating mathematics with the philosophy of mathematics – they are two distinct disciplines. Disagreements about the philosophy of mathematics make no direct difference to mathematics itself; at the margins, they can influence judgements about which problems are interesting – although, even there, a person can find ultrafinitist mathematics interesting without needing any philosophical commitment to an ultrafinitist philosophy of mathematics.

> 2^512 exists in binary notation, but not in unary notation (tally marks, successor function).

Sorry, but this is incoherent nonsense. The existence of a number doesn't depend on its representation ... but we can in fact represent any integer 0 > SHA-512 depends on the fact that computers cannot feasibly increment to 2^512.

non sequitur

> A loop cannot feasibly run 2^512 times.

non sequitur

> Strict finitists emphasize those distinctions when they say 2^512 doesn't exist.

Cranks.

I’m aware of constructive math. You still have the type of natural numbers in that?

A few formalizations exist: bounded arithmetic, internal set theory, Nelson's predicative arithmetic.

From Buss's thesis "Bounded Arithmetic": "However, a recursive function may be computable only in a theoretical sense: the time required to compute it may be far larger than the lifespan of the universe. We are more interested in feasibly computable functions, which can be calculated by today's (or tomorrow's) computers."

And then he goes and defines an arithmetic hierarchy for polynomial functions.