I was reading "constructive analysis" by Bishop and right on page 15 he writes "The relation of equality given above for rational numbers is an equivalence relation. In this example there is a finite, mechanical procedure for deciding whether or not two given objects in the set are equal. Such a procedure will not exist in general: there are instances in which we are unable to decide whether or not two given elements of a set are equal;" but then right in the next paragraph he insists that functions need to have a finite, mechanical procedure to be valid constructively.
What makes me confused is why do we let equivalence relations not be decidable, it seems that if we were to fully commit to constructivism we should make everything constructive on the offset. Can someone explain to me why this isn't the case?
I have not looked at the Bishop book, but I am going to take a guess. This is an analysis text, so we consider the real numbers.
A real number can be understood as an infinite sequence of digits (modulo the equivalence that makes $0.999\ldots = 1.000\ldots$). Constructively it does not make sense to think of an infinite sequence of digits as a single, completed object. Instead, we imagine a process that can generate as many digits as we want. Think of an algorithm for computing digits of $\sqrt 2$. We can't know $\sqrt2$ exactly, but we can know it to any desired precision.
Now let's suppose we have two real numbers, $a$ and $b$. It makes perfect sense, constructively, to say that we know $$a,b\in \Bbb R$$ because we have in hand processes that will produce rational approximations of $a$ and $b$ to any desired precision.
But something strange happens when we try to compare $$a\stackrel?= b.$$ If the numbers are unequal, we can be certain to detect that: at some point we will have generated enough digits of each number to find a place where they differ.
But if the numbers are equal, that never happens, and we will never become certain. We might have found that the first million digits of each number are the same, but we still don't know that they won't differ sometime later. All we can ever say is that $a$ and $b$ are equal to within some precision.
So in this sense, the $=$ relation is not decidable on real numbers! Nevertheless we can certainly recognize a real number when we have one, and we can perform computations with real numbers, such as addition and multiplication, in the sense that we can describe a process that will produce as many correct digits as we want of the sum or product.
You ask:
This is making everything constructive. The goal is to do mathematics with a more accurate model of what can actually be computed. We want to do real analysis. That involves the real numbers. Conventional mathematics claims that the real numbers have a decidable equality relation. Constructive mathematics denies this, because we cannot always compute numeric results with perfect precision.