Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!usc!ucselx!bionet!parc!mdixon From: mdixon@parc.xerox.com (Mike Dixon) Newsgroups: comp.object Subject: Re: Global program state. Message-ID: Date: 7 Jan 91 00:51:36 GMT References: <330@coatimundi.cs.arizona.edu> <2474@motcsd.csd.mot.com> Sender: news@parc.xerox.com Organization: Xerox PARC, Palo Alto, CA Lines: 48 In-Reply-To: lance@motcsd.csd.mot.com's message of 4 Jan 91 03:18:46 GMT 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. asserting that "true" is equivalent to "provable" is a pretty extreme philosophical position. i suspect you haven't really thought about where it leads to; most people find the consequences unacceptable. if you're familiar with meta-mathematics, the point of godel's proof was precisely that there are true statements (in number theory) that can't be proven. if you're interested in less abstract things (e.g. whether or not the disk gets reformatted), it seems even less acceptable to equate "provable" with "true". personally, i think the point of proofs (and other forms of reasoning, formal or informal) is to give us some information about what the world is like. in the case of program correctness, a proof helps me figure out whether or not the program is correct, but doesn't *make* it correct. in particular, as soon as you start writing proofs about subjects other than number theory or geometry, you realize that proofs simply give you a relation between one set of assumptions about the world (the "axioms") and another set (the "conclusions"); they certainly don't give you any magic handle on truth. Prove the Mac works. C'mon, I dare you. good example. think about it. what would a proof tell you? note that a) i can prove the mac works trivially, if i chose the right axioms (of course, that proof doesn't give me any confidence that it really will work) b) no matter what axioms you choose, the existence of a proof won't guarantee that the mac will actually do what the documentation says it ought to do (at the very least, your axioms will make assumptions that the hardware functions correctly) c) (back to the original topic of this thread) you're not going to simplify this proof by eliminating "global state", since what matters about the mac's behavior is precisely this state (i.e. what's displayed on the screen, what's written to the disk, etc.). -- .mike.