> There are non-computable objects that mathematicians study.
What's an example of such a non-computable object? Constructionism is based on the fact that every proof is a construction, which corresponds to a program, so you're claiming that there are proofs that do not correspond to any construction/program, and I'm curious what that might look like.
> Constructionism is based on the fact that every proof is a construction, which corresponds to a program
I don't think this is correct, even in constructive logic. Negative statements do not correspond to a construction, and in fact are the only statements in constructive logic that may be proven "by contradiction". But this means that every statement of non-constructive logic can be understood "constructively", if in a rather trivial sense, as a negative statement.
Linear logics may be a good way of exploring these issues in depth, since these allow for explicit "constructions" while preserving the sort of 'duality of negation' (i.e. flipping the direction of implications, or exchanging conjunctions w/ disjunctions) that's quite familiar within classical logic. Somewhat relatedly, there's also an interesting question of how much "construction" really is involved in typical constructive proofs, and whether that can be cleanly separated out from the more purely "logical" parts of the proof.
You're right that I'm being a little loose with terminology, as when I say "constructivism" I mean something more like "intuitionism", as with type theory.
Intuitionistic logic also allows for negative statements, which then are entirely non-constructive.
From a proofs-as-programs POV, this is just the observation that a proof is not just a program, but rather a program plus an explanation of why that program works correctly within its constraints, e.g. why it never ever tries to divide by zero. (This can be rephrased by saying that the program is both requesting and providing abstract "capabilities", i.e. information-free tokens, to its environment. Classical logic is then the logic of these capabilities, in the sense that providing a weak capability as output is essentially the same as asking for a strong capability from your environment as input.)
The theorem that every vector space has a basis, something that is used fairly often, is actually equivalent to the axiom of choice, something that isn't valid in constructive logic. For many vector spaces you won't be able to write down a basis. And there are other examples, e.g. almost none of the automorphisms of C can be written down (only the identity and the conjugate map).
I'm aware that constructivism is not mainstream. What you've described are that such constructions are not available at this time (not comparable ones), but is there any evidence that comparable constructions are not possible even in principle?
This is exactly what I'm talking about, "every vector space has a basis" is not a provable statement in constructive mathematics because that ranges over non-constructive objects, but it can prove constructive equivalents like "every finite-dimensional or countable vector space has a basis".
I'm just not persuaded that this is not sufficient for any realizable mathematical construction. In my view, some non-constructive objects are non-realizable and so must ultimately serve only as convenient shortcuts that are ultimately eliminated when the math manifests in a real construction, either physical or computational. So if such things are merely artifacts of a particular formalism, then it should be possible to dispense with them entirely with a constructive or intuitionistic formalism.
That's why I'm looking for something that truly, fundamentally impossible for constructive mathematics, but that we know to exist, be true, valid, etc. that would contradict this position.
Using the law of the excluded middle is definitely a shortcut in such proofs, but there is no proof I'm aware of that shows no comparable constructive proof is possible. We reason with non-computable objects all of the time, such constructions are simply never fully materialized, and the need to materialize them are typically eliminated in later stages to prove concrete results. It's a good example but I don't think it's sufficient to exclude math from computer science.
What's an example of such a non-computable object? Constructionism is based on the fact that every proof is a construction, which corresponds to a program, so you're claiming that there are proofs that do not correspond to any construction/program, and I'm curious what that might look like.