[6gvONxR4sf7o]

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?

[Kranar]

You are absolutely correct and you have discovered Rice's Theorem [1]. The fact that you generalized the halting problem on your own is a very good indication that you fundamentally understand it.

[1] https://en.wikipedia.org/wiki/Rice%27s_theorem

[6gvONxR4sf7o]

I certainly do feel like I understand it better now. Thanks again for the pointers!