I'm glad I haven't seen that then. But conversely it does annoy me to see classical mathematicians dogmatically claim as true statements that depend on their philosophy. And that I have seen a lot of.

As for the specific complaint, once you have Constructivism, Banach Tarski falls apart (even in versions with the axiom of choice). So if you don't like the weirdness, there is no need to accept it. (But you won't get advanced degrees in math unless you can at least temporarily pretend to accept it. Zorn's lemma is just too widely used.)

But can we agree to both dislike people who argue that 0.999... is not 1?

You can account for and "do" classical math perfectly fine as a constructivist+finitist. It just means that any statements about non-constructive existence or non-decidable choice must be phrased as negative statements in the logic; positive disjunction or existentials are reserved for anything that's decidable/constructible.

And uses of the axiom of choice are viewed with suspicion even by many who are doing perfectly classical math, so there's nothing wrong with pointing them out as assumptions ("if we admit of choice being applicable to X, we have Y").

In theory, maybe. In practice you have to work to reconcile the constructive "all functions are continuous" with classical results like "a strictly increasing function can be discontinuous on a dense set." (The two disagree on what a function is.)

As for choice, try doing much functional analysis without Zorn's lemma.

There are parts of math that you can do constructively. But most of it you really can't. And choice is embedded in a lot more math than you'd guess.

> In theory, maybe. In practice you have to work to reconcile the constructive "all functions are continuous" with classical results like "a strictly increasing function can be discontinuous on a dense set." [T]he two disagree on what a function is.

Well yes, it's still a different kind of math. What's not true however is this common notion that a constructivist can only ever view all "classical" math as pure nonsense. In many ways, it ought to be a lot easier for someone committed to constructivist semantics to grok a classical development than the converse - because decision procedures, computations etc. are way more of an afterthought to mainstream mathematicians.

That's why for me, constructivism - or in general mathematics with different axioms - are additions to classical mathematics, not replacements. And in that sense, they're fine for me. You'll definitely find people online defending the position that all classical maths is bullshit - I'm not saying that actual researchers behave like that, though.

But I'm also a strict formalist, or more accurately, I think whichever axioms happen to be useful should be used, without much need for there to be a epistemological commitment.