3 ms·

That's not a thing. The problem isn't self referential statements. The problem is much larger, and self referential statements are the easiest way to construct

That's not a thing. The problem isn't self referential statements. 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. Trying to construct a mathematical system of axioms is like trying to construct the most powerful system of computation possible that isn't subject to the halting problem. You want to prove stuff, so you want a powerful system. Eventually, you end up with a system of axioms that is so powerful it can prove contradictory results, or you end up with a language where you cannot prove it halts or does not halt. You want to not be able to prove untrue true, and you want true things to be unable to be proven false, so you weaken your tools. Either you fail to weaken your tools enough, or you eventually end up unable to prove true statements are true. In programming, the fact that it's unprovable that a program halts isn't actually a big deal. 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. (usually, and if not, it's the customer's problem, not mine) That doesn't work in math. In math, if you want to publish a paper that proves x, you want to be sure that nobody's going to publish a paper proving !x anytime soon. So you need a restricted language, unlike programmers. It turns out banning self referential statements makes it really, really hard to prove stuff.

strbean 7y ago
> 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)".
- dllthomas 7y ago
  > 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.
- dllthomas 7y ago
  > 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.

strbean 7y ago

> 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)".

dllthomas 7y ago
> 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.
dllthomas 7y ago
> 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.