Anonymous user
Talk:Proof: Difference between revisions
→J version: rants
(→Draft status: new section) |
(→J version: rants) |
||
Line 117:
:::::::::::::: Great. It's still not a proof, though. What's next? You're going to claim you've proved the Collatz conjecture because you have checked the first 9 cases using a J program? Now, if you managed to pull that feat using Coq there's probably both a Turing Award and a Fields Medal waiting for you. —''[[User:Ruud Koot|Ruud]]'' 20:38, 10 May 2012 (UTC)
::::::::::::::: No. I made no claims about the Collatz conjecture. --[[User:Rdm|Rdm]] 20:44, 10 May 2012 (UTC)
:::::::::::::::: No you didn't, but your method is equally applicable. I used it to prove [[wp:Goldbach's conjecture|Goldbach's conjecture]]:<lang text> even + even = even even = prime + prime
-----------------------------------------------------------------------------------------
1. Print sum of a bunch of even numbers, Print even numbers from 4 to a billion,
show that they are all even; show that they are each sum of two primes;
2. Argue that step 1 is "convincing", induction schminduction;
3. (backup plan) Dare any disagreeing reader to find a counter example;
4. Profit! I mean, proof!</lang>
:::::::::::::::: Your arguments thoughout this discussion varied, but none of them justfies the J example as a proof:
:::::::::::::::: 1. "The task didn't say what kind of proof it wants": it doesn't matter. What J offers is anecdotal evidence, not a proof. You can't quote a nameless math teacher to subvert the well-agreed meaning of a word, not when the context is programming/math/logic.
:::::::::::::::: 2. "Authors of the pdf I linked says machine proof/program verification sucks": it's true. I mean, they did say that. So?
:::::::::::::::: 3. "Coq/Adga/whatever's output still requires the reader to understand it": true. It also requires the reader to know what mathematical induction is. But if you ''can'' read it, you'll see that it's done the way how a human would have proved it, with the critical "for any number n, it can be reduced to..." thingy, which no amount of integer printout can replace.
:::::::::::::::: 4. "Rosettacode tasks should allow every language to participate": I don't believe so. It's good to have a task that's applicable to most languages, but tasks tailored towards a handful specific languages are worthwhile, too. Case in point: it's good to show readers how a proof assistant works; barging in with something completely irrelevant like the J example is very unhelpful.
:::::::::::::::: All in all, it's pretty clear what the task wanted, and that the J example didn't deliver. When a task is asking for something your language is not designed for or is incapable of doing, the decent thing to do is: nothing. Just omit the task. --[[User:Ledrug|Ledrug]] 22:07, 11 May 2012 (UTC)
== Draft status ==
| |||