Okay, you got me thinking about this more generally, and it seems like this sort of proof can disprove all sorts of checkers: function HasPropertyX(A: (S:

Okay, you got me thinking about this more generally, and it seems like this sort of proof can disprove all sorts of checkers: function HasPropertyX(A: (S: string) => void, S: string): boolean; function Q(S: string): void { if(HasPropertyX(Q, S)) { AvoidHavingX(); } else { HaveX(); } } For example, no program can exist that checks whether another program raises an exception on some argument (pseudocode, since I don't really know typescript): function RaisesException(A: (S: string) => void, S: string): boolean; function Q(S: string): void { if(RaisesException(Q, S)) { pass; } else { raise Exception; } } and no program can exist that determines whether a given bit of code blows up the planet: function BlowsUpThePlanet(A: (S: string) => void, S: string): boolean; function Q(S: string): void { if(BlowsUpThePlanet(Q, S)) { pass; } else { HitTheBigRedButtonAndGoKaboom(); } } and you can't even test whether f(x) is true: function ReturnsTrue(A: (S: string) => boolean, S: string): boolean; function Q(S: string): boolean { return not ReturnsTrue(Q,S); } It seems like it any property you can exhibit in HaveX cannot be checked for, leading me to think that this is a proof that you can't definitively check for pretty much anything in programs, but that seems too far. Am I getting this right? How far does this go? Is there a deeper theorem about the limitations of program checking that brings this all together?