Talk:Proof: Difference between revisions

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