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?