How do you prove these string/number radix encoding/decoding algorithms work?
First, you need to figure out what it is you want to prove. Here, I'd say we want to prove that
toString(parseInt(x, code),code) = x
and
parseInt(toString(x, code),code) = x
It's pretty obvious that trying to prove this is going to fail if:

we overflow the result in parseInt, because then parseInt isn't surjective
the input in parseInt contains characters that aren't in the code

So, our proof has to include the assumption that both are not the case.
The first proof is probably easier than the second. We can do induction on the length of `value':
toString(parseInt(x, code),code) = x
Given an arbitrary code which contains all characters in x
If x.length == 0:

x == ''
parseInt(x, code) returns 0
toString(0, code) returns ''  &lt;- actually it returns 'a' so the proof breaks here, but you can do the same if you assume length 1

If x.length &gt; 1

our induction hypothesis: for all prefixes y of x toString(parseInt(y, code),code) = y
parseInt(x, code) = parseInt(x[:-1], code) * code.length + code.indexOf(x[-1])   (I am using python syntax here to say everything but the last element, and the last element. This in and of itself would have to be proved I guess but it would be very easy if the algorithm was written recursively instead of iteratively)
toString(a * code.length + b, code) = code[b] + toString(a, code)  (again, this would be straightforward if the algorithm was recursive, but it should be convincing enough that this is the case here)
that means toString(parseInt(x,code),code) = toString(parseInt(x[:-1], code) * code.length + code.indexOf(x[-1]), code) = code[code.indexOf(x[-1])] + toString(parseInt(x[:-1], code), code) = (using induction hypothesis) x[-1] + x[:-1] which breaks our proof because toString has a bug and inverts the string, as far as I can tell.

Assuming the line result = code[digit] + result actually read result = result + code[digit] like I think it should:

toString(a * code.length + b, code) = toString(a, code) + code[b]  (again, this would be straightforward if the algorithm was recursive, but it should be convincing enough that this is the case here)
that means toString(parseInt(x,code),code) = toString(parseInt(x[:-1], code) * code.length + code.indexOf(x[-1]), code) = toString(parseInt(x[:-1], code), code) + code[code.indexOf(x[-1])] = (using induction hypothesis) x[:-1] + x[-1] = x

QED.
The other direction is similar, you can again use induction as long as you take care that your induction hypothesis is &quot;for all y &lt; x: parseInt(toString(y, code),code) = y&quot;.