[zozbot234]

> As far as I understand it, classical mathematics is non-constructive.

It's not as simple as that. Classical mathematics can talk about whether some property is computationally decidable (possibly with further tweaks, e.g. modulo some oracle, or with complexity constraints) or whether some object is computable (see above), express decision/construction procedures etc.; it's just incredibly clunky to do so, and it may be worthwhile to introduce foundations that make it natural to talk about these things.

[smj-edison]

Would it be fair to say then that classical mathematics does not require computability, so it requires a lot more bookkeeping, while intuitionistic logic requires constructivism, so it's the air you live and breathe in, which is much more natural?

[zozbot234]

Intuitionistic logic is not really constrained to talking about constructive things: you just stuff everything else in the negative fragment. Does that ultimately make sense? Maybe, maybe not. Perhaps that goes too far in obscuring the inherent duality of classical logic, which is still very useful.