Ah, thanks for clarifying! I think I overlooked the "square root" part of your original response. You're right, seeing the source code is no help at all! And it

Ah, thanks for clarifying! I think I overlooked the "square root" part of your original response. You're right, seeing the source code is no help at all! And it's difficult to say that a human could always say if sqrt(x) is rational, for all x. Still, this seems a bit like the Goldbach conjecture example: we don't have a math proof for this now, but some day we might. I wonder if there is any program that is provably undecidable---like the way Godel's theorem proves that some statements are undecidable from their axioms.