This is true, but it has a problem: if you prefer constructive logic to classical because it is "finer-grained", then where do you stop? Linear logic, for exam

This is true, but it has a problem: if you prefer constructive logic to classical because it is "finer-grained", then where do you stop? Linear logic, for example, is finer-grained than both classical and constructive logic. Both can be embedded in it (just as classical embeds into constructive), and it makes distinctions they lack. But linear logic, too, comes in classical and intuitionistic versions, and again classical linear logic embeds into intuitionistic. And it doesn't stop there. Linear logic can be embedded in ordered logic, and ordered logic into the logic of bunched implications. For all I know there are even finer-grained logics out there. But doing all of mathematics in the logic of bunched implications would be an impractical nightmare, I think. I tend to prefer choosing whether to work classically or constructive (or linearly, or orderedly) according to whether it illuminates a relevant part of the problem. Sometimes you care about constructivity; sometimes you don't. If you don't, then don't waste your time trying to do the proof constructively. The trouble, of course, is that you don't always know whether working constructively will provide illumination until you try it! :)