Nice. So here we have two testcases that catch different bugs, and you can never prove the absence of bugs by adding more testcases. But testing still works well enough in practice that people rarely write fully formal proofs for software, or for math theorems for that matter :-)
Our disagreement seems to derive from my use of the words “different flawed step” and your use of “same flaw”. Eliezer suggested substituting 1 for x and y in :
(x+y)(x-y) = y(x-y)
x+y = y
yielding
(1+1)(1-1) = 1(1-1) (true)
1+1 = 1 (false)
Thus, since a true equation was transformed into a false one, the step must have been flawed.
Under my suggestion, we have:
(0+0)(0-0) = 0(0-0) (true)
0+0 = 0 (true)
So, under Eliezer’s suggested criterion (turning true to false) this is not a flawed step, though if you look carefully enough, you can still notice the flaw—a division by zero.
So, under Eliezer’s suggested criterion (turning true to false) this is not a flawed step, though if you look carefully enough, you can still notice the flaw—a division by zero.
Hmm. A failure to identify a flawed step doesn’t mean that the step isn’t flawed.
A true statement turning into a false one does show that you manipulated it badly—but a true statement staying true doesn’t show that you manipulated it well.
Amusingly, try substituting x=y=0. You find a different flawed step than the one Eliezer found.
Nice. So here we have two testcases that catch different bugs, and you can never prove the absence of bugs by adding more testcases. But testing still works well enough in practice that people rarely write fully formal proofs for software, or for math theorems for that matter :-)
Actually, x=y=0 still catches the same flaw, it just catches another one at the same time.
Our disagreement seems to derive from my use of the words “different flawed step” and your use of “same flaw”. Eliezer suggested substituting 1 for x and y in :
yielding
Thus, since a true equation was transformed into a false one, the step must have been flawed.
Under my suggestion, we have:
So, under Eliezer’s suggested criterion (turning true to false) this is not a flawed step, though if you look carefully enough, you can still notice the flaw—a division by zero.
Hmm. A failure to identify a flawed step doesn’t mean that the step isn’t flawed.
A true statement turning into a false one does show that you manipulated it badly—but a true statement staying true doesn’t show that you manipulated it well.
Hah, this is pretty good :-)