Anonymous user
Talk:Proof: Difference between revisions
→The Go proof?: long rantish discussion
(→The Go proof?: compilers are programs too) |
(→The Go proof?: long rantish discussion) |
||
Line 51:
: The task might be poorly worded and poorly named, but I think the examples posted by the task author and every example except Haskell show the same thing, which is using the language type system enforcement of closure over a type as an analog of mathematical closure over a set of numbers. The code to demonstrate isn't the code that you write, but the code that is in the language translator. —[[User:Sonia|Sonia]] 01:09, 22 June 2011 (UTC)
::I'm not sure what you meant by the last sentence (actually, I'm not sure what you meant by the sentence before that one, either). As to other examples, Coq seems to be doing the right thing; TCL seems to be doing the right thing (or pretending to, I can't tell); Haskell seems to be doing a slight variant of the right thing. Of the other ones, Adaga and Omega do seem to only define a set without verifying it's closed, if so they are incorrect, too, but I don't know enough about them to say for sure. Unfortunately, I do know what the Go code does.
::It is capable of verifying (when run) if <i>any given instance of</i> a number is even, doing so by recursion to individual instances of predecessors, not induction based on definition, which is a big difference. Your other argument, that if it passed compiler type checking, it must be consistent, is false: my bogus "oddPeano" passed it with gaping logic holes, and the compiler didn't catch it, because it's not supposed to. True that if I read the code, I may say "that's not going to work, the hasPredecessor() will go past one and reach -1 and below", but a) I'm not the compiler; b) the task requires the program to prove, not "let Ledrug read the code and prove".
::Now if the we can change the task description to say "show by examples that such and such", your code is perfectly fine (again, if you run it). As it is, though, it's not enough as a proof.
::Lest I look too harsh, I'm not trying to be overly righteous or trying to kill your fun; it just so happens that I think "prove" is not a verb to be used slightly. --[[User:Ledrug|Ledrug]] 02:09, 22 June 2011 (UTC)
| |||