4 ms·

Honestly this objection always seemed very handwavey to me, especially given how much abuse the incompleteness theorems endure during extension beyond statement

by ahelwer 10y ago

Honestly this objection always seemed very handwavey to me, especially given how much abuse the incompleteness theorems endure during extension beyond statements about the Natural numbers. Like, what exactly happens if you try to write a bootstrapped theorem prover? Does a deity descend from the heavens to unplug your keyboard? I'd be very interested in reading a paper or blog post documenting a practical attempt here.

lmkg 10y ago
The incompleteness theorem effectively states that some statements will require an infinite amount of time for this bootstrapping approach to work. The only deity involved is the finite-ness of the natural world.
simondedalus 10y ago
I don't mean to be rude, but this objection only seems handwave-y if you don't understand Gödel's proofs (common), or you have some refutation of them (obviously uncommon, but definitely interesting). This is a good not-too-technical but not-condescending explanation https://www.amazon.com/G%C3%B6dels-Proof-Ernest-Nagel/dp/0814758371 https://www.amazon.com/G%C3%B6dels-Proof-Ernest-Nagel/dp/081... (it does get into the technical details; it just doesn't go line by line as you would if you wanted to recreate the proofs). As long as you have the expressive power of Peano arithmetic (which all programming languages ought to, and definitely all proof systems ought to), you can find a Gödel sentence in the system and thus prove that it can't prove, of itself, "x is consistent". It's worth looking into, if only for the enjoyment.
- hinkley 10y ago
  Have you ever written a compression algorithm? You do know that Shannon proved that general purpose compression is impossible, right? Why bother if that 75% compression ratio is provably impossible?
- ahelwer 10y ago
  It isn't at all obvious that "a theorem prover proving itself correct" and "an axiomatic system proving its own consistency" are the same thing, beyond both being in the category of things which refer to themselves in the domain of mathematical proofs. Software correctness isn't the same as consistency. A program is correct if it refines its specification, and an axiomatic system is consistent if it does not lead to contradiction. Before doing a deep dive into Gödel we need to firmly establish we're actually looking at the right problem. Even if Gödel is shown to apply in the strict generalized theoretical sense, it might be irrelevant to practice. Theory and practice often differ enough for practice to be very useful; we easily prove halting for most programs we care about, compute solutions to average-case NP-Complete problems without a noticeable rise in CPU temp, and (as the other poster at this level said) write compression algorithms which work well on all relevant inputs. This is poor analogous reasoning, of course, but I include it because demonstration of universal practical pitfall would be very interesting in much the same way specific manifestations of availability loss in fault-tolerant consensus algorithms are interesting. Really though, I am tired of the above exact exchange playing out in every thread I've seen here on formal verification. Someone raises the obvious concern of bugs in the theorem prover. Someone else raises the bootstrapping solution, cribbed from compilers. Someone else raises the Gödel objection; and there the conversation dies. Dig deeper.
  - nickpsecurity 10y ago
    Good write-up. I hear you about the patterns of debate that prop up in these threads. My favorites are the ones where people show up with specific logics, techs, or R&D suggestions that others and I learn from. Such an approach might lead to people solving hard problems over time. My favorite counter to the Godel thing, esp about termination, was sklogic showing how far from reality these concerns were by illustrating that a while loop counting down toward zero with "stop if zero" condition will guarantee a termination of any algorithm working piece-by-piece in inner loop so long as hardware functions. No magic math at all required to defeat the termination requirement in real-world. I added watchdog timers or even shelf-life of modern parts can do the same. I did something similar when I was concerned about infinite loops or DOS attacks from malicious input. Just box it up in something I know will work with something checking up on it. Another was algorithm theory telling me QuickSort performed better but choose HeapSort if worst-case is a problem. A smarter programmer told me to just time average for QuickSort, run it with a watchdog, kill it on any instance it takes too long, and use HeapSort for that instance. Those are the kind of tips I appreciate about these terrible problems the theoretical side brings me. Hell, if only theory people would find, generalize, and expand on all the effective cheats in engineering instead of idealistic or abstract stuff. :)

by ahelwer 10y ago

lmkg 10y ago

The incompleteness theorem effectively states that some statements will require an infinite amount of time for this bootstrapping approach to work. The only deity involved is the finite-ness of the natural world.

simondedalus 10y ago

I don't mean to be rude, but this objection only seems handwave-y if you don't understand Gödel's proofs (common), or you have some refutation of them (obviously uncommon, but definitely interesting). This is a good not-too-technical but not-condescending explanation https://www.amazon.com/G%C3%B6dels-Proof-Ernest-Nagel/dp/0814758371 https://www.amazon.com/G%C3%B6dels-Proof-Ernest-Nagel/dp/081... (it does get into the technical details; it just doesn't go line by line as you would if you wanted to recreate the proofs). As long as you have the expressive power of Peano arithmetic (which all programming languages ought to, and definitely all proof systems ought to), you can find a Gödel sentence in the system and thus prove that it can't prove, of itself, "x is consistent". It's worth looking into, if only for the enjoyment.

hinkley 10y ago
Have you ever written a compression algorithm? You do know that Shannon proved that general purpose compression is impossible, right? Why bother if that 75% compression ratio is provably impossible?
ahelwer 10y ago
It isn't at all obvious that "a theorem prover proving itself correct" and "an axiomatic system proving its own consistency" are the same thing, beyond both being in the category of things which refer to themselves in the domain of mathematical proofs. Software correctness isn't the same as consistency. A program is correct if it refines its specification, and an axiomatic system is consistent if it does not lead to contradiction. Before doing a deep dive into Gödel we need to firmly establish we're actually looking at the right problem. Even if Gödel is shown to apply in the strict generalized theoretical sense, it might be irrelevant to practice. Theory and practice often differ enough for practice to be very useful; we easily prove halting for most programs we care about, compute solutions to average-case NP-Complete problems without a noticeable rise in CPU temp, and (as the other poster at this level said) write compression algorithms which work well on all relevant inputs. This is poor analogous reasoning, of course, but I include it because demonstration of universal practical pitfall would be very interesting in much the same way specific manifestations of availability loss in fault-tolerant consensus algorithms are interesting. Really though, I am tired of the above exact exchange playing out in every thread I've seen here on formal verification. Someone raises the obvious concern of bugs in the theorem prover. Someone else raises the bootstrapping solution, cribbed from compilers. Someone else raises the Gödel objection; and there the conversation dies. Dig deeper.
- nickpsecurity 10y ago
  Good write-up. I hear you about the patterns of debate that prop up in these threads. My favorites are the ones where people show up with specific logics, techs, or R&D suggestions that others and I learn from. Such an approach might lead to people solving hard problems over time. My favorite counter to the Godel thing, esp about termination, was sklogic showing how far from reality these concerns were by illustrating that a while loop counting down toward zero with "stop if zero" condition will guarantee a termination of any algorithm working piece-by-piece in inner loop so long as hardware functions. No magic math at all required to defeat the termination requirement in real-world. I added watchdog timers or even shelf-life of modern parts can do the same. I did something similar when I was concerned about infinite loops or DOS attacks from malicious input. Just box it up in something I know will work with something checking up on it. Another was algorithm theory telling me QuickSort performed better but choose HeapSort if worst-case is a problem. A smarter programmer told me to just time average for QuickSort, run it with a watchdog, kill it on any instance it takes too long, and use HeapSort for that instance. Those are the kind of tips I appreciate about these terrible problems the theoretical side brings me. Hell, if only theory people would find, generalize, and expand on all the effective cheats in engineering instead of idealistic or abstract stuff. :)