Computer science ought to be about computation, right? There are non-computable objects that mathematicians study. Is that part of 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.
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.
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).