In the general case, it is impossible to create an algorithm that confirms whether an algorithm is equivalent to a specification. This is an informal proof:
Almost all programming languages are Turing-complete. Therefore, any language decided by a TM can be also be decided by a program written in this language.
The problem of determining whether two TMs accept the same language, known as $Equivalence/TM$ is undecidable. As a consequence of Turing completeness, the same holds for the programs of the given language. In other words, it is undecidable to know whether the inputs you want your program to accept and the inputs it really does are the same.
Furthermore, $Equivalence/TM$ is not even recursive enumerable. That is because $Non-emptiness/TM$ (whether a TM accepts at least one input) is an acceptable language, since you can iterate over all possible inputs. If the TM is non-empty, eventually you will find a word that is accepted. Therefore $Emptiness/TM$ is unacceptable, otherwise $Emptiness/TM$ would be decidable (which we know it is not). However Emptiness/TM can be reduced to $Equivalence/TM$, therefore $Equivalence/TM$ is also unacceptable. Therefore you can use an algorithm whether or not two machines are not equivalent, but you cannot be sure if they are equivalent, or you haven't given your algorithm enough time.
However, this is only for the general case. It is possible that you can decide whether or not the specifications are equivalent to the program, by solving a more relaxed version of the problem. For example, you might examine only a number of inputs or say that the two programs are equivalent with some uncertainty. This is what software testing is all about.
As for the rest of your questions:
Note: This part has been edited for clarification. It turns out that I did the mistake I was trying to avoid, sorry.
Let $TrueR$ be the collection of languages that we know to be decidable. Of course $TrueR \subseteq R$. One can then prove the following:
$ProvableR = TrueR$. It is easy to see that $ProvableR \subset TrueR$. However, it is also $TrueR \subset ProvableR$ . The proof is very easy: Let $A \epsilon TrueR$ . By definition , in every input $A$ returns either YES or NO. Therefore, $A$ halts on every input. It follows that $A \epsilon ProvableR$ .
Informally , this can be summarized as: You don't know that a language is decidable until you have proven it to be. So if in a formal system you have the knowledge that a language is decidable, this knowledge can also serve as a proof for that. Therefore, you cannot simultaneously have the knowledge that a language is both decidable and it cannot be proven so, these two statements are mutually exclusive.
My final point is that our knowledge is partial and that the only way of studying $R$ is through $ProvableR$. The distinction might make sense in mathematics and we can acknowledge it, but we possess no tools to study it. Since $ProvableR \subset R$ , we are bound to never completely know $R$ in its entirety.
@Kaveh summarizes it best: Provable always means provable in some system/theory and does not coincide with truth in general.
The same holds for any other complexity class: To determine membership you need a proof first. This is why I believe that your second question is too general, since it contains not only complexity theory, but also computation theory as well, depending on the property you want the language to have.