Why Has None of Computer Science been Formalized?
in [Logic]
|
Prev: Simple yet Profound Metatheorem
Next: Modal Logic
From: Steven Zenith on 14 Sep 2006 15:59 Charlie-Boo wrote: > ... > > 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. Maybe. However, it is the business model of the software industry today. > ... > > 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. I guess I am missing what exactly you are looking for. I have already pointed to examples of specific results 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. Apologies, I've noted elsewhere that I meant to say here "functions of the kind you describe." Your answer depends upon the specification of a function and the implementation. Such a function "may" terminate immediately leaving the result undefined or randomly defined. > > One can easily program side effect free functions in any language. Where are the tools to formally verify this and where are the language specifications so well formed as to allow this? Not C or C++, maybe Java? > But > why would that prevent the application of formal methods anyway? These > side effects are merely additional semantics. The point is that most available programming languages are semantically weak when related to both their intrinsic structure and the exceptions allowed by their implementation. Few compilers or interpreters are rigorously formal - and, surprisingly, neither are the optimizers. Typing is not strictly enforced of changes range from implementation to implementation. Side effects can perhaps be viewed as additional semantics. But your view is naive, rarely are side effects consistent with the programming model specification and will lead to nondeterminism quickly - so the best way to address them is to eliminate them from the language in the first place. I clearly have not pickup on the particular problem you are trying to solve. Later I'll look back over what you have said. With respect, Steven
From: Jack Campin - bogus address on 14 Sep 2006 16:45 > 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. So you just add a second argument to the sqrt function saying how many places of precision you want. That two-argument function does terminate, and there's no implementation dependence about it. There was also a fair bit of work on programs that acted as filters on streams - it presumably suffered the same commercial fate as your stuff, but it went a long way towards incorporating interactive software like operating systems and user interfaces into the functional model. (At one point in the 1990s, Microsoft hired a team of people who knew the state of the art in that area - god knows what they did with them, maybe somebody ought to dig up a few of the drains around Redmond). ============== 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: Steven Zenith on 14 Sep 2006 17:12 Jack Campin - bogus address wrote: >... > So you just add a second argument to the sqrt function saying how many > places of precision you want. That two-argument function does terminate, > and there's no implementation dependence about it. Well, you have now placed the implementation dependence in the new argument. It is better to explicitly express a pragmatic, I agree, but these pragmatics will play hell with the formal system unless differentiated from the algorithmic goals. With respect, Steven
From: Rupert on 14 Sep 2006 17:13 Charlie-Boo wrote: > Rupert wrote: > > Charlie-Boo wrote: > > > Rupert wrote: > > > > Charlie-Boo wrote: > > > > > Do we all agree that Computer Science definitely should be formalized? > > > > > > > > > > > > > What's the merit in being completely formal, for any branch of > > > > mathematics? Surely it's enough to convince ourselves that we could > > > > formalize it. > > > > > > Why develop mathematics? > > > Because it's interesting. > > > > Why have people axiomatized branches of mathematics? > > > To clarify the foundations of the reasoning. > > > > > Is it better to have a single representation for a theorem rather than > > > many equivalent representations? > > > Not clear to me why one should be better than the other. > > The merit in being completely formal is that it accomplishes the above. It's not necessary in order to accomplish the above. It's extra work that serves no particularly useful function. > > C-B
From: Charlie-Boo on 15 Sep 2006 03:10
george wrote: > 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. Trivial? No man, it depends on what you're trying to formalize. And trivial or not, who has ever come up with a formalization of any branch of Computer Science - Program Synthesis, Theory of Computation, Recursion Theory or Incompleteness in Logic? What book or article describes a general system for generating the theorems in any of these? > > You are saying that it can be formalized, but Godel didn't. > > Yes, he did -- didn't you read the other replies. Which theorems does his system generate? You don't get to claim success without showing that success. One article with one proof "formalized" does not constitute a general means of generating theorems in some area of study. C-B |