Talk:Proof: Difference between revisions
→Scope of Task
No edit summary |
|||
Line 139:
:: To make it clear, I look at this J code from the sideline, I don't really understand it, but when I see such inconsistencies I just started to doubt about the whole approach. Can you give some references? What is the "kernel" that you are implementing? It is consistent? — [[User:Ht|Ht]] 17:44, 6 June 2012 (UTC)
::: I disagree (obviously). Most languages include a variety of techniques for displaying strings, and we do not expect to see all of them illustrated in a "Hello World" task. We only expect to see one of them illustrated. Strings are not a good analogy here, though, because most languages include extensive support for strings, and most languages do not include extensive support for proofs. Also, historically, a proof has always been specific to a single theorem. We do not expect that a proof for associativity of addition for peano numbers will be valid for complex numbers or quaternions -- we demand a separate proof.
::: You did find a bug in my earlier implementation, where it was inconsistent -- it was treating different free variables as identical, but I have fixed that bug.
::: Anyways, there's a reason that Knuth once warned: "Beware of bugs in the above code; I have only proved it correct, not tried it." It's trivial to find cases where systems proven correct via denotational semantics will fail in practice. The axioms are not a valid reflection of the machine implementation, and a proof necessarily is only valid when its axioms are valid. --[[User:Rdm|Rdm]] 18:50, 6 June 2012 (UTC)
== Huh? ==
| |||