> The problem is much larger, and self referential statements are the easiest way to construct a counterexample. Self referential statements are a symptom, not a cause.
I'm curious, though, if things like the halting problem actually hold in the absence of (certain types of) self-referential statements. To my (very limited) knowledge, all proofs in these areas rely on them.
> Most of the normal problems we deal with don't need algorithms which probe the boundaries of halting, and QA picks up the stuff we miss.
But QA gets a bunch of excuses derived from the halting problem! For example:
> Boss: We have A which works, and we wrote B that is much faster, make sure they are functionally identical.
> QA: I can write a lot of tests, run fuzzers, but actually proving that A == B is undecidable!
Also, partially as a consequence of the halting problem, running untrusted code in a sandbox inherently means setting hard timeouts.
> It turns out banning self referential statements makes it really, really hard to prove stuff.
I'm not advocating for stripping out reflection from whatever system. Just saying (based on dumb gut feelings) that maybe we've stopped short of valuable results on things like "The halting problem (ignoring that one gotcha)".
> QA: I can write a lot of tests, run fuzzers, but actually proving that A == B is undecidable!
A == B is undecidable for some choice of A and B. It's may very well not be for the particular A and B that you've handed to QA.
In a practical sense, though, it's worth noting that the excuse doesn't really derive from theoretical undecideability.
What we really care about is "can the benefit here be worth the cost". Depending on how you look at it, when it's undecidable there's infinite cost or no benefit, so in that case the answer is clear. But there are probably arbitrarily hard problems shy of undecidable. We occasionally solve math problems that people tens or hundreds of people have been working hard on for decades - those weren't undecidable.
> I'm curious, though, if things like the halting problem actually hold in the absence of (certain types of) self-referential statements. To my (very limited) knowledge, all proofs in these areas rely on them.
I mean, if "certain types of self-referential statements" we're banning can include all recursion and (dynamic) loops, then the halting problem is trivial - your program halts.
I'm curious, though, if things like the halting problem actually hold in the absence of (certain types of) self-referential statements. To my (very limited) knowledge, all proofs in these areas rely on them.
> Most of the normal problems we deal with don't need algorithms which probe the boundaries of halting, and QA picks up the stuff we miss.
But QA gets a bunch of excuses derived from the halting problem! For example:
> Boss: We have A which works, and we wrote B that is much faster, make sure they are functionally identical. > QA: I can write a lot of tests, run fuzzers, but actually proving that A == B is undecidable!
Also, partially as a consequence of the halting problem, running untrusted code in a sandbox inherently means setting hard timeouts.
> It turns out banning self referential statements makes it really, really hard to prove stuff.
I'm not advocating for stripping out reflection from whatever system. Just saying (based on dumb gut feelings) that maybe we've stopped short of valuable results on things like "The halting problem (ignoring that one gotcha)".