How to prove that replacing a character in a string in both C and JavaScript is equivalent?
I would start by creating a formal definition of the function that you want and then proving for correctness each of the implementations.

Consider the following axiomatic definition:

$$replaceAt: string * \mathbb Z *char \to string$$ 

$$\forall c:char . ( \forall i \in \mathbb Z~.~replaceAt(``,i,c) = `` )$$

$$\forall c:char . (\forall s:string . ( \forall i \in 0.. len(s)-1~.~replaceAt(s,i,c)[i] = c ))$$

$$\forall c:char . (\forall s:string . ( \forall i \in 0.. len(s)-1~.~len(replaceAt(s,i,c)) = len(s) ))$$

$$\forall c:char .(\forall s:string . ( \forall i,j \in 0..len(s)-1 . i \neq j \implies replaceAt(s,i,c)[j] = s[j] ))$$

$$\forall c:char .(\forall s:string . ( \forall i \in \mathbb Z . i \geq len(s) \implies replaceAt(s,i,c) = s ))$$

If you can prove the correctness of each implementation to these axioms I'd say they're equivalent. At the moment your C implementation is not even a function.  Your Javascript function takes a string and not a char.  None of them are defined for indexes greater than your input.   

I don't think comparing implementation to implementation makes sense as there are lot of differences in the implementation models of each language.