Path: utzoo!censor!geac!torsqnt!news-server.csri.toronto.edu!cs.utexas.edu!usc!zaphod.mps.ohio-state.edu!think.com!paperboy!macrakis From: macrakis@gr.osf.org (Stavros Macrakis) Newsgroups: comp.object Subject: Re: Global program state. Message-ID: Date: 4 Jan 91 14:30:25 GMT References: <330@coatimundi.cs.arizona.edu> <2474@motcsd.csd.mot.com> Sender: news@OSF.ORG Organization: OSF Research Institute--Grenoble Lines: 37 In-reply-to: lance@motcsd.csd.mot.com's message of 4 Jan 91 03:18:46 GMT 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 apparently assuming that `works' is equivalent to `works perfectly'. Why should the verb `to work' mean something different for programs than for (say) mechanical cash registers, corkscrews, or rocket launchers? None of them work all the time, yet we can say that they `work'. It has been argued that programs must be proven to work because they are mathematical objects. But what will the proof prove? Only that they correspond to their mathematical specification. And what proves that the mathematical specification corresponds to the desired behavior? This is only possible in narrow fields. I am certainly not arguing against proving (some) properties of (some) programs. This can be interesting in many cases and can even be cost-effective in some cases. However, an unproved program can still be useful. I would say it `works'. -s Stavros Macrakis Open Software Foundation Research Institute Mail: 2 av de Vignate, 38610 Gieres (Grenoble), France Net: macrakis@gr.osf.org Phone: +33/76.63.48.82 Fax: +33/76.51.05.32