As best I can tell the article wrongly conflates Rices Theorem with the idea that one can’t prove something about the small program generated by Yedidiya and Aaronson but that’s not what Rices Theorem tells us. Instead it tells us that we can’t come up with a general method to determine yes or no correctly for all programs whether a program reaches a given point.

For a given program and a one off proof one can prove many things or if we over approximate by assuming loops terminate we can prove many things soundly with the risk of rejecting programs that are sometimes correct (eg type systems).

This may have been a quirk of language or my interpretation though.

Yes, moreover - nobody in practice creates programs that are close to be undecidable, just like no engineer uses nonmeasurable functions, they just assume everything is nicely integrable. (It might be close to true for things like cryptographic functions or pseudorandom generators, but even about these we can usually prove the things we need to know.)