Why Has None of Computer Science been Formalized?
in [Logic]
|
Prev: Simple yet Profound Metatheorem
Next: Modal Logic
From: Steven Zenith on 13 Sep 2006 04:02 Charlie-Boo wrote: > Do we all agree that Computer Science definitely should be formalized? > > While the definitions of common terms (e.g. recursively enumerable) are > formal, the manipulations of these concepts (e.g. the derivation of > proofs) is not. ... This is simply incorrect. Much work has been done in the formalization of Computer Science and that work continues to be taught at various universities as far as I am aware. Especially see the work of Roscoe, Hoare (CSP) and Milner - and many others from a variety of camps. I am personally aware of a number of proofs that illustrate interesting formal properties of programs - including properties such as deadlock freedom and that programs meet their specifications - and of the tools that enabled the demonstration of same. That these tools have not continued to be widely developed, have only had limited availability and have not been broadly applied is, frankly, deplorable. With respect, Steven -- Dr. Steven Ericsson-Zenith IASE, Sunnyvale, California
From: Peter_Smith on 13 Sep 2006 06:01 > Step D, An algorithm for generating formal statements such as A, has > been studied in the form of axioms and rules of inference. But here we > are doing all of A-F. We need to show that the theorem proven > corresponds to a certain published theorem, what expressions in general > mean, how it was proven, and how we know the system is sound. > > You can start with A, A formal statement of the theorem or result. This is in not a cogent response. I made the absolutely standard claim that, while the the first incompleteness theorem was proved by informal reasoning (outside the formal type theory P which Gödel was originally considering), there is a formal rendering of its conclusion into the language of P via arithmetization. Gödel *claimed* that this formal rendering Th has a formal proof inside P, and Hilbert and Bernays later *showed* that it did. You asked what "formal proof" meant here, and I responded: nothing other than the standard textbook sense -- Th follows from the axioms of the formal system P by the deductive rules of P. By all means if your are interested in other sorts of "proof", boojum proofs lets call them, then of course you are welcome to tell us about boojum proofs, explain why we should be interested in boojum proofs etc. etc. Just fine. But the notion of a formal proof has a perfectly well understood technical sense in logic: and in that utterly standard technical sense, Hilbert and Bernays indeed showed that Th has a formal proof inside P. End of story.
From: Alec McKenzie on 13 Sep 2006 06:27 "Charlie-Boo" <shymathguy(a)gmail.com> wrote: > Alec McKenzie wrote: > > > In which case you must have meant to say "A formal proof that in > > every programming language there is a program that outputs > > itself". > > > > It seems clear to me that that cannot be true > > Why? A single counter-example is sufficient: consider a programming language for writing screen-savers to display pretty moving pictures of coloured patterns, and these moving patterns are the only output that a program written in that language is able to produce. Since the program itself is not a moving coloured pattern, it follows that no program in that programming language can output itself. So not "every programming language...". -- Alec McKenzie usenet@<surname>.me.uk
From: Charlie-Boo on 13 Sep 2006 08:10 guenther vonKnakspot wrote: > Charly Boo Boo wrote: > <snip yet another proof of his ignorance> > > C-B > > You are joking, right Boo Boo? Let's see. We have: 1. An unsubstantiated claim about a missing snippette. 2. An unsubstantiated claim about missing additional examples. 3. A question regarding these missing snippettes and examples. I guess my answer will have to be missing as well. C-B PS My middle name isn't Boo. The English translation of my last name, Bew (German for "proof") is Boo (pronounced "buh-you" not "boo".)
From: Charlie-Boo on 13 Sep 2006 08:27
Steven Zenith wrote: > Charlie-Boo wrote: > > Do we all agree that Computer Science definitely should be formalized? > > > > While the definitions of common terms (e.g. recursively enumerable) are > > formal, the manipulations of these concepts (e.g. the derivation of > > proofs) is not. ... > > This is simply incorrect. > > Much work has been done in the formalization of Computer Science and > that work continues to be taught at various universities as far as I am > aware. Especially see the work of Roscoe, Hoare (CSP) and Milner - and > many others from a variety of camps. I am very interested in any examples of this. Can you give one, including: A. A formal statement of the theorem or result. B. The meaning of any such statement. C. How A corresponds to the statement of the theorem. D. An algorithm for generating formal statements such as A. E. A demonstration that D generates A. F. A demonstration that D generates only true statements. What I have discovered is that the manner in which these problems are formulated is faulty, resulting in a lot of energy being spent (as you describe) wasted. For example, much work has been spent trying to construct programs by building the flowchart. This is at the wrong level of abstraction. The details are unimportant - only the fact that the program as a whole computes a particular result is relevant. Working at this higher level of abstraction, we can manipulate programs as units, rather than trying to make sense out of their internal structure. Similarly, in Proof Theory the characterization of relations using systems of logic has focused on particular bases for that characterization: expressible, representable, contrarepresentable. However, what is needed is a more general model in which the base is a variable. > I am personally aware of a number of proofs that illustrate interesting > formal properties of programs - including properties such as deadlock > freedom and that programs meet their specifications - and of the tools > that enabled the demonstration of same. > > That these tools have not continued to be widely developed, have only > had limited availability and have not been broadly applied is, frankly, > deplorable. It is because nobody has ever shown these approaches to produce anything. Give a single simple example of solving a programming or theoretical problem using formal methods as taught in universities. (Note A-F above.) C-B > With respect, > Steven > > -- > Dr. Steven Ericsson-Zenith > IASE, Sunnyvale, California |