Talk:Proof: Difference between revisions

Line 145:

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

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

:::: Yes, we know that anything can be printed in conventional languages just as anything (what is truth) can be proved in theorem proving systems.

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

:::: It's a good analogy because I do not consider conventional languages at all. I am only talking about proof systems, in them we can show a simple proof and expect that one can prove any theorem the same way (e.g. [https://gist.github.com/1286093/8ff1afbc8b8f8aef051349eda19ccaec193c902d here] is a proof of Euclid's theorem in Agda). In weak conventional language, on the other hand, nothing can be proved, only proof system can be written.

:::: > Also, historically, a proof has always been specific to a single theorem.

:::: Historically has been almost a hundred years since the advent of formal logic (Boole, Peano, Dedekind, Hilbert, Frege, Russell, Whitehead, Quine, Cantor, Zermelo, Fraenkel, Löwenheim, Skolem, Gödel, Gentzen, Tarski works) in which theorems is just sequences of symbols derivable by rules of inference from axioms and a proof is an algorithm of deriving. And more than fifty years since the advent of сomputability theory and formulation of the Church-Turing thesis and the Curry-Howard correspondence (Church, Kleene, Turing, Gödel, Post, Rosser, Curry works). Type Theory is a further development. [http://video.ias.edu/voevodsky-80th Quoting] Voevodsky mathematical logic is just a combinatorial game, which, of course, can be implemented as software, as proof system suitable for proving any theorems.

:::: I remind that you have not explained [[wp:Proof_theory|what]] is the kernel that you are implementing. Propositional calculus, FOL, — [[User:Ht|Ht]] 15:44, 7 June 2012 (UTC)

== Huh? ==