cousin_it comments on Making Reasoning Obviously Locally Correct - Less Wrong

19 Post author: JGWeissman 12 March 2011 07:41PM

You are viewing a comment permalink. View the original post to see all comments and the full post content.

Comments (23)

You are viewing a single comment's thread. Show more comments above.

Comment author: Perplexed 12 March 2011 09:35:07PM 5 points [-]

Amusingly, try substituting x=y=0. You find a different flawed step than the one Eliezer found.

Comment author: cousin_it 13 March 2011 02:06:33PM *  3 points [-]

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 :-)