I thought it was sorting an infinite set of infinite strings as the first step in the "algorithm" that seemed sketchy. [0]

It's definitely not a constructive proof, even though it pretends to be; none of the mathematical objects can be constructed, nor can any of the algorithmic steps be executed.

That said, it's far less well-known that the workaround (if you find it to be true) is trivially easy (from Alfred Tarski), making it kind of a useless theorem in practice.

[0] You might think, well, I'll just write out the strings in order by using a generator! No sorting needed... But you have to write the strings down to perform the algorithm, and it takes infinite time to write down the first string, so you'll never even get to the others which is when you do the diagonalization trick. Like I said: it's not constructive, none of it can actually be done.