Talk:Proof: Difference between revisions
→J version
(→J version: re) |
|||
Line 93:
:::::: As most programming languages correspond to an unsound logic the answer to "what are they proving" is usually "nothing". I think it's generally good advice to make a task widely applicable/implementable, but in this particular case it is not. The task's intention is to demonstrate the difference in syntax and semantics of the 15 or so proof assistants currently in existence. This is useful and clearly in line with Rosetta Code's mission. Adding 100 "faked" solutions of languages never intended to be used as a proof assistant is not. Those solutions add no value and distract from the information that is there. Finally, also note that the Agda, Coq and Twelf solutions implement the exact same thing, while the J solution seems very different.—''[[User:Ruud Koot|Ruud]]'' 15:20, 10 May 2012 (UTC)
::::::: I disagree with your opening sentence unless it is further qualified with
"because the user does not understand what is happening".
::::::: As for the last sentence, that cannot be a problem in and of itself.
::::::: More specifically, when dealing with a concept like "Natural Numbers", a computer cannot represent them in their entirety. Instead, we have to accept some symbol which represents them. And, thus, when we deal with a "proof about Natural Numbers" we are really dealing not with natural numbers but with a surrogate. The surrogate can have only a subset of all properties of natural numbers. A question then, in the context of a proof is: does the mechanical implementation represent all relevant properties of natural numbers in the surrogate? In the context of "even" and "odd" all of the relevant properties are present in single digit decimal numbers (and by this, I mean that you are not going to be able to demonstrate any relevant exceptions, without going outside the bounds of this task).
::::::: Thus, your point seems to be that you want the task to be expressed in a system which expresses the relevant rules using a particular system of symbols, and you want the task to demonstrate that the language uses the "proper sorts of manipulation" of those symbols. But that has problems: (a) the task does not really define what is "proper", and (b) as near as I can tell, a person would have to study the language implementation to determine whether treatment of [for example] induction with excluded middle is handled adequately. --[[User:Rdm|Rdm]]
| |||