Anonymous user
Talk:Proof: Difference between revisions
→J version: re
(→J version: re) |
|||
Line 82:
::: 3) It's not clear to me that this narrow of a definition of proof is valid in the context of rosettacode. For it to be valid it would have to be shown that your restricted concept of proof does not exclude most programming languages.
::: --[[User:Rdm|Rdm]] 14:17, 10 May 2012 (UTC)
::::# I think the boldfaced note expresses this, although the task description can indeed be made more clear.
::::# You're confusing things here. The Coq program here ''is'' a proof (one that can be verified by the compiler to be correct!). Clearly the reader needs to understand some things about Coq to understand exactly what has been proven, but this is no different from most samples in any other task and quite different from what (I believe) the J, Go and Tcl samples are doing: they give a program and the instruct the reader to mentally construct some kind of correctness proof.
::::# On the contrary, this task explicitly excludes the majority of languages. I don't see a problem with this at all. Because most languages are Turing-complete an algorithmic or computational task can be implemented in nearly any language. However there also exist tasks that concern the abstraction or other languages facilities which simply cannot be reasonably implemented in any language. E.g. one can imagine tasks that only make sense in either dynamically-typed or statically-typed languages, languages having a sufficiently expressive type system or supporting reflection. Adding "fake" solutions only distracts the reader from the thing the task is trying to demonstrate or compare.
:::: —''[[User:Ruud Koot|Ruud]]'' 14:48, 10 May 2012 (UTC)
| |||