Question about the undecidability of $A_{TM}$
If you know what the program is doing, you can predict its outcome even without running it. For example, consider the following program.

INPUT: a polynomial P with integer coefficients
n = 0
while P(n) is different from zero:
  n = n + 1


This program halts if the input polynomial $P(x)$ has a non-negative integer root. It turns out that this problem is decidable - there is a clever shortcut that determines the outcome of the program. How can we rule out the existence of such shortcuts in general? The proof you describe is one clever way of doing that.