Why Has None of Computer Science been Formalized?
in [Logic]
|
Prev: Simple yet Profound Metatheorem
Next: Modal Logic
From: Steven Zenith on 20 Sep 2006 12:05 Charlie-Boo wrote: .... > I still don't see any examples of theorems from Computer Science being > formally generated. We can spend a lifetime going through hundreds of > internet web sites in search of this. But you tell me that you are > aware of it already - so why not tell me here what you are referring > to? That would take only 5 minutes. > > What is the theorem that is formally generated? What is its formal > representation? What is the sequence of formal steps that lead to its > construction? Can you just give a few lines here? Then you will have > proved your point. Why not? Like you I am a little frustrated that the links at these sites have not been maintained. Here is Geoff Barrett's ACM account of the case I have pointed to. http://portal.acm.org/citation.cfm?coll=GUIDE&dl=GUIDE&id=65476 I am also surprised that on returning to the question after many years that this case remains the most referenced instance of the application of formal methods and that there are not more case studies readily available. But to your repeated questions, this case meets your criteria. I have mentioned the steps that were taken already to verify the floating point implementation in silicon of the IEEE Floating Point standard. The theorem is an equivalence between specification and implementation. The steps were transformations between three formal entities: the IEEE Spec, the Occam description of the implementation, and the hardware specification that implements Occam. The formalism at each level (as I recall) were Z, CSP/Occam, HDL. In any case, must one not assume that the groups applying these tools are meeting your criteria? For what is the point of a formal system such as Z or CSP if it is not to generate theorems about interesting properties of programs and to take the formal steps to construct a proof of them? One area of computer science that is well formalized is the field of concurrency and communication. I haven't seen you mention Shannon. With respect, Steven
From: Charlie-Boo on 20 Sep 2006 12:47 Steven Zenith wrote: > http://portal.acm.org/citation.cfm?coll=GUIDE&dl=GUIDE&id=65476 This is only an abstract. What is the theorem? What is the formal representation of the theorem? What is the sequence of steps (or at least the first few and the last few) that construct the formal representation of the theorem? Why won't you give it here? I have given examples of CBL proofs. I continue to offer to present here the formal derivation of any of the theorems that I have mentioned and other related theorems that anyone wants: Godel 1931, Rosser 1936, Turing 1937, Kleene 1950's, Smullyan 1960-2000, Program Synthesis of Number Theoretic functions. Why don't you? C-B > With respect, > Steven
From: Jack Campin - bogus address on 20 Sep 2006 13:39 > I still don't see any examples of theorems from Computer Science being > formally generated. Any time you see a piece of software created using a yacc grammar verifying that an input text is syntactically correct, that's exactly what you're getting. ============== j-c ====== @ ====== purr . demon . co . uk ============== Jack Campin: 11 Third St, Newtongrange EH22 4PU, Scotland | tel 0131 660 4760 <http://www.purr.demon.co.uk/jack/> for CD-ROMs and free | fax 0870 0554 975 stuff: Scottish music, food intolerance, & Mac logic fonts | mob 07800 739 557
From: george on 20 Sep 2006 16:10 > > Charlie-Boo wrote: > > > You have to tell in advance an exact algorithm that creates every > > > proof. I replied, > > That this is trivial is PRECISELY what Godel's proof proves. CB, digging his hole deeper... > Trivial? No man, it depends on what you're trying to formalize. NO, Charlie, it cannot DEPEND on what we are trying to formalize, because "what we are trying to formalize" is not VARYING! WE KNOW what we are trying to formalize! YOU SAID, >*>*> an exact algorithm that creates every >*>*> proof. ^^^^^^^^^ So PROOF is what we are trying to formalize. And 1st-order proof-predicates are PRIMITIVE-recursive. It is EASY to tell whether an alleged proof is one or isn't one, at least it's easy compared with THE LENGTH of the proof. Put another way, proofs can be long, but they CAN'T be hard.
From: Charlie-Boo on 20 Sep 2006 20:02
Jack Campin - bogus address wrote: > > I still don't see any examples of theorems from Computer Science being > > formally generated. > > Any time you see a piece of software created using a yacc grammar > verifying that an input text is syntactically correct, that's exactly > what you're getting. Then why does the user have to type it in if the computer generates it automatically? Answer: Same answer as why nobody has posted an example of a formally generated result from Computer Science despite my asking for one dozens of times for over a year. (Can you see the reason? It's not rocket science.) C-B > ============== j-c ====== @ ====== purr . demon . co . uk ============== > Jack Campin: 11 Third St, Newtongrange EH22 4PU, Scotland | tel 0131 660 4760 > <http://www.purr.demon.co.uk/jack/> for CD-ROMs and free | fax 0870 0554 975 > stuff: Scottish music, food intolerance, & Mac logic fonts | mob 07800 739 557 |