Why Has None of Computer Science been Formalized?
in [Logic]
|
Prev: Simple yet Profound Metatheorem
Next: Modal Logic
From: Alec McKenzie on 14 Sep 2006 14:38 "Charlie-Boo" <shymathguy(a)gmail.com> wrote: > Alec McKenzie wrote: > > "Charlie-Boo" <shymathguy(a)gmail.com> wrote: > > > > > Alec McKenzie wrote: > > > > > > > > I see you are back to the existence of "*a* self-outputting > > > > program", the proof of which is trivial (i.e. a single example > > > > will do it). > > > > > > No, you have to prove the program exists for every programming > > > language, not just one. > > > > Which cannot be done, since the program does *not* exist for > > every programming language, as can be very easily shown. > > How do you define "Programming Language"? That's why we differ (I > assume i.e. that you would agree using the same definition as I.) It seems you would like to define "Programming Language" as one in which a self-outputting program exists. That is not a definition I would agree with. -- Alec McKenzie usenet@<surname>.me.uk
From: Steven Zenith on 14 Sep 2006 15:01 I meant to say "functions of the kind you describe terminate" - obviously, recursive functions - such as those that may produce irrational numbers - do not necessarily terminate. This "determinism," or lack of it, is another subject covered by Roscoe and co. in the 1980s. Sincerely, Steven Steven Zenith wrote: > Charlie-Boo wrote: > > ... > > > It is not that these projects did not produce compelling results - we > > > did, and to international acclaim > > > > What is the significance of "acclaim"? > > Merely in the sense that the results were widely recognized. > > Before judging this work, and much like it, that took place in the > formal methods community at least between 1950 and 1990, I suggest that > you read some of it. > > No one is suggesting that not to use these techniques is corrupt - it > has simply an associated economic pragmatic that has been important > during a very competitive era. When time to market is no longer > important companies will be prepared to spend the upfront time to > formally engineer their code. And there is the rub in much of your > comments. I don't really see what you are after in the computer science > sense if you are not after the application of formal methods to > engineering. If you are rather looking for abstract principles of > computational theory, that seems to be less an engineering task as a > general task in logic and there is plenty on literature in that domain. > > Formal methods very often deal with the obvious. In logic of course a > function terminates, that assumption cannot be made in computer science > since one needs to understand the implementation and the machine > architecture. > > When I refer to Standards - I am referring to industry standards for > protocols and interfaces - few of which provide a formal specification. > To verify an implementation of such a standard I not only need a > formal spec but also a formally verified target platform. > > That you do not understand this about termination and that you cannot > readily identify issues that prevent the ready application of formal > methods to conventional languages - side effect free functions perhaps > being the most obvious - I again suggest you read the literature. > > With respect, > Steven
From: Charlie-Boo on 14 Sep 2006 15:12 Steven Zenith wrote: > Before judging this work, and much like it, that took place in the > formal methods community at least between 1950 and 1990, I suggest that > you read some of it. >From the OP: "Curry-Howard, Manna/Waldinger, Boyer/Moore, Modal Logic, Prologue and TPTP all attempt to do this, but nobody has ever shown any examples of anything near A-F." Why do you say that I need to read "some of it"? > No one is suggesting that not to use these techniques is corrupt. No, rather that "A quick and dirty solution today for which I can charge endless consulting fees to maintain" is corrupt. > I don't really see what you are after in the computer science > sense if you are not after the application of formal methods to > engineering. Who said I wasn't? > If you are rather looking for abstract principles of > computational theory, that seems to be less an engineering task as a > general task in logic and there is plenty on literature in that domain. Again you refer to articles being written, but not a single example of a result being formally produced. > Formal methods very often deal with the obvious. In logic of course a > function terminates, that assumption cannot be made in computer science > since one needs to understand the implementation and the machine > architecture. A function that is undefined on a particular input is considered to be the result of a program that does not terminate on that input. > That you do not understand this about termination and that you cannot > readily identify issues that prevent the ready application of formal > methods to conventional languages - side effect free functions perhaps > being the most obvious - I again suggest you read the literature. You're saying that no popular programming language is free of side effects? One can easily program side effect free functions in any language. But why would that prevent the application of formal methods anyway? These side effects are merely additional semantics. I believe that non-terminating programs are in fact represented by undefined functions, and so it is you who does not understand. But that is getting personal! By what reasoning can you say that there is relevant literature that I have not read? If it is relevant, then give an example of a formally generated result in Computer Science that is described. That is the question. Can you do that? C-B > With respect, > Steven
From: Steven Zenith on 14 Sep 2006 15:23 For further clarification: A function that computes the square root of 2 is a good example of a non-terminating function. In what formal computational sense can it be said to terminate? Logically, none. However, pragmatically, we know that implementations terminate by at some point producing an approximation of the function - these pragmatics will vary from implementation to implementation. Programs dependent on such results will vary in their behavior. Sincerely, Steven Steven Zenith wrote: > I meant to say "functions of the kind you describe terminate" - > obviously, recursive functions - such as those that may produce > irrational numbers - do not necessarily terminate. This "determinism," > or lack of it, is another subject covered by Roscoe and co. in the > 1980s. > > Sincerely, > Steven > > > Steven Zenith wrote: > > Charlie-Boo wrote: > > > ... > > > > It is not that these projects did not produce compelling results - we > > > > did, and to international acclaim > > > > > > What is the significance of "acclaim"? > > > > Merely in the sense that the results were widely recognized. > > > > Before judging this work, and much like it, that took place in the > > formal methods community at least between 1950 and 1990, I suggest that > > you read some of it. > > > > No one is suggesting that not to use these techniques is corrupt - it > > has simply an associated economic pragmatic that has been important > > during a very competitive era. When time to market is no longer > > important companies will be prepared to spend the upfront time to > > formally engineer their code. And there is the rub in much of your > > comments. I don't really see what you are after in the computer science > > sense if you are not after the application of formal methods to > > engineering. If you are rather looking for abstract principles of > > computational theory, that seems to be less an engineering task as a > > general task in logic and there is plenty on literature in that domain. > > > > Formal methods very often deal with the obvious. In logic of course a > > function terminates, that assumption cannot be made in computer science > > since one needs to understand the implementation and the machine > > architecture. > > > > When I refer to Standards - I am referring to industry standards for > > protocols and interfaces - few of which provide a formal specification. > > To verify an implementation of such a standard I not only need a > > formal spec but also a formally verified target platform. > > > > That you do not understand this about termination and that you cannot > > readily identify issues that prevent the ready application of formal > > methods to conventional languages - side effect free functions perhaps > > being the most obvious - I again suggest you read the literature. > > > > With respect, > > Steven
From: george on 14 Sep 2006 15:38
Charlie-Boo wrote: > You have to tell in advance an exact algorithm that creates every > proof. That this is trivial is PRECISELY what Godel's proof proves. 1st-order consequence is recursively enumerable. There is an algorithm that (your choice) recursively enumerates proofs (there are only a finite number of proofs of length n, for any n), or confirms that a candidate proof submitted as input is in fact elected when it is in fact a proof (if it's not a proof, the algorithm might not terminate). > You are saying that it can be formalized, but Godel didn't. Yes, he did -- didn't you read the other replies. He didn't say he could or was doing it, but he did say it was doable. Hilbert and Bernays in fact shortly thereafter did it. IT HAS been done. The question is not whether it's been formalized; it's just whether it is computer science. |