Why Has None of Computer Science been Formalized?
in [Logic]
|
Prev: Simple yet Profound Metatheorem
Next: Modal Logic
From: Steven Zenith on 30 Sep 2006 12:37 Charlie-Boo wrote: .... > > Because that is not my level of participation here. You made a claim > > and I pointed you to work that I believed countered the claim - you > > have not, to my satisfaction, acknowledged the information I provided. > > Yes I did. I read it and it doesn't contain what you say. ... Then there is some misunderstanding, and perhaps our use of English differs. I understood that you where looking for areas of Computer Science that were formalized. I pointed you at work that does indeed formalize an area of Computer Science - essentially the work of Hoare and Milner that focus on concurrency and communication. Both formalisms are general purpose process algebras. I also pointed to the specification language Z (based on Zermelo-Fränkel set theory) as a related general purpose Computer Science formalism. I also pointed you at practical instances where these formalisms have been applied to prove important properties of programs - we discussed verification, termination and deadlock freedom as examples of such properties. These are the formal results that I referred to. If you have read the books I referenced, as you say, then this should be clear: there is at least one area of computer science that has been formalized and there are formal results that come from those efforts. Now, I thought that I had clarified this but you appear to be asking for something else. With respect, Steven
From: Charlie-Boo on 30 Sep 2006 12:49 Steven Zenith wrote: > What I saw there reminded me of Robin Milner's CSS. When you get to the > library ask for this book: > > http://www.amazon.com/Communication-Concurrency-Prentice-International-Computer/dp/0131150073/sr=8-1/qid=1158936360/ref=pd_bbs_1/002-2129589-0385604?ie=UTF8&s=books > > And while you are at it ask for the reference I gave you in the first > place: > > http://www.amazon.com/Theory-Practice-Concurrency-W-Roscoe/dp/0136744095/sr=1-2/qid=1158936562/ref=sr_1_2/002-2129589-0385604?ie=UTF8&s=books Sorry, but I don't see it in there. What are your referring to - what formal derivation of a result from Computer Science? Thanks. > As to you other comments I will confess to being mystified. I have in > previous postings complied with you request to state the theorem, > formalism and technique of proof. The specific example, a case study, > demonstrated the general case for the formal methods tools we used. It is quite the leap to go from a manually generated analysis of one problem to a general, formal means of generating solutions to a whole class of such problems. You realize that, don't you? That is like saying that each person who proves a theorem in some subject has just given a system for automatically generating all of them! C-B > With respect, > Steven
From: Charlie-Boo on 30 Sep 2006 13:08 Steven Zenith wrote: > Charlie-Boo wrote: > ... > > > Because that is not my level of participation here. You made a claim > > > and I pointed you to work that I believed countered the claim - you > > > have not, to my satisfaction, acknowledged the information I provided. > > > > Yes I did. I read it and it doesn't contain what you say. ... > > Then there is some misunderstanding, and perhaps our use of English > differs. > > I understood that you where looking for areas of Computer Science that > were formalized. I pointed you at work that does indeed formalize an > area of Computer Science - essentially the work of Hoare and Milner > that focus on concurrency and communication. Both formalisms are > general purpose process algebras. I also pointed to the specification > language Z (based on Zermelo-Fränkel set theory) as a related general > purpose Computer Science formalism. > > I also pointed you at practical instances where these formalisms have > been applied to prove important properties of programs - we discussed > verification, termination and deadlock freedom as examples of such > properties. These are the formal results that I referred to. > > If you have read the books I referenced, as you say, then this should > be clear: there is at least one area of computer science that has been > formalized and there are formal results that come from those efforts. > > Now, I thought that I had clarified this but you appear to be asking > for something else. You are giving a lot of titles, but these are not systems that formally derive theorems from Computer Science. You need to show that it does what you say. The books do not. Maybe if you simply gave the formal representation of the theorem that you have in mind and its formal derivation, that would show everyone why you believe what you say. It would certainly prove your point. That is normally how mathematical results are conveyed - by presenting, along with the claim, a proof of that claim so that the readers of the claim also see the proof along with it. We really can't read your mind as to what in particular you believe is an example of a formal representation of a theorem and its derivation. : ) So far your posts have consisted of only informal English. (Personally, I suspect that it is simply an honest misunderstanding on your part of what these systems really do. Presenting your own understanding with an example of what you personally think constitutes a formal representation of a theorem and its derivation, should clear the air. You certainly have exhibited much misunderstanding regardng fundamentals of Mathematics, such as the nature of real numbers and irrational numbers in particular, as a number of people have pointed out in this thread.) C-B > With respect, > Steven
From: Steven Zenith on 1 Oct 2006 04:24 Charlie-Boo wrote: > (Personally, I suspect that it is simply an honest misunderstanding on > your part of what these systems really do. Presenting your own > understanding with an example of what you personally think constitutes > a formal representation of a theorem and its derivation, should clear > the air. You certainly have exhibited much misunderstanding regardng > fundamentals of Mathematics, such as the nature of real numbers and > irrational numbers in particular, as a number of people have pointed > out in this thread.) Of course, even great mathematicians can make mistakes :-) With respect, Steven
From: Steven Zenith on 1 Oct 2006 04:37
Charlie-Boo wrote: .... > Maybe if you simply gave the formal representation of the theorem that > you have in mind and its formal derivation, that would show everyone > why you believe what you say. It would certainly prove your point. > > That is normally how mathematical results are conveyed - by presenting, > along with the claim, a proof of that claim so that the readers of the > claim also see the proof along with it. I do not see how such a demonstration is relevant here. All that was necessary was to show where computer science has been formalized - it was not actually necessary to perform the formalization. Similarly, it was only necessary to indicate the results and not necessary to perform them - especially since neither the formalism or the results that were being defended. I have met the standards of your request, which simply made an informal claim that no area of computer science had been formalized. After reviewing the materials I pointed you toward, do you still claim that this is the case? I did perhaps misunderstand, in that I understood that the theorems you were looking for were those of practical application but it seems you were looking to repeat well-known results in logic. This may be interesting as a case study of some new formalism - but it hardly constitutes a new contribution to the field. With respect, Steven |