[H8crilA]

This is obviously a joke by Vitalik Buterin, also it's a good test as to whether someone actually understands the proof :)

If you know the proof you probably know that you don't actually use the "(n+1) mod 10" mapping, you use that mapping but instead remap all 8's into something else, like 3, in particular you don't remap 8's into 9's to avoid the "99999..." tail problem. In fact if you like you can just use the following mapping: 0->1, {1,2,3,4,5,6,7,8,9}->0. Also, for the starting representations you simply replace all expansions with an infinite tail of "9999...", as for every such representation there exists a representation that does not end in "9999...". This makes the decimal expansions unique.

All the name-able reals are obviously countable, this has a deep connection with the Löwenheim–Skolem theorem: https://en.wikipedia.org/wiki/L%C3%B6wenheim%E2%80%93Skolem_...

[comonoid]

I think the error is much deeper here: he presumes that every number in R can be produced by a program, i.e. every real number is computable.

[H8crilA]

That is, I think, the second part of the joke, all required to "prove" the thesis at the end, namely that halting problem is solvable :)