Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!swrinde!zaphod.mps.ohio-state.edu!usc!petunia!news From: jdudeck@polyslo.CalPoly.EDU (John R. Dudeck) Newsgroups: comp.object Subject: Re: Global program state. Message-ID: <2784e0a8.6cc8@petunia.CalPoly.EDU> Date: 4 Jan 91 20:08:08 GMT References: <330@coatimundi.cs.arizona.edu> <2474@motcsd.csd.mot.com> Organization: Cal Poly State Univ,CSC Dept,San Luis Obispo,CA 93407 Lines: 30 >In article <2474@motcsd.csd.mot.com> lance@motcsd.csd.mot.com (lance.norskog) writes: > No, I don't consider the millions of working programs a counter-example, > because I don't consider them to work. > > A program doesn't "work" because you (or somebody) thinks it works. > A program "works" if it can be mathematically proven to work. Experience > and operational time don't count. This isn't like quantum physics where > observation decides the matter. Empirical evidence doesn't enter into it. You are evidently a purist. In mathematics, certainly a theorem can't be said to be true until it is proven. But I don't think it is possible to insist that programming is essentially a mathematical exercise (despite the attempts of many to do so). I believe programming and software engineering is more of a management problem than it is a mathematical activity. The management of complexity can be performed without the explicit statement of formal specifications and the explicit application of formal proofs or a program transformation calculus. We do it all the time. But that doesn't mean that our programs would fail if submitted to a formal proof. The problem is not that the programs don't work, it's that our specification languages and our proof methods don't work. -- John Dudeck "If it's Object Oriented then by jdudeck@Polyslo.CalPoly.Edu definition it's A Good Thing". ESL: 62013975 Tel: 805-545-9549 -- D. Stearns