gsmith@garnet.berkeley.edu (Gene W. Smith) (01/11/90)
There has already been one request to get this crap out of sci.math. Not only do you jerks not listen, this subject is still cross-posted to a zillion other irrelevant groups. Put this rubbish in comp.theory where it belongs, and try to remember that not everyone on the net is a CS weenie. -- ucbvax!garnet!gsmith Gene Ward Smith/Brahms Gang/Berkeley CA 94720 "You and I as individuals can, by borrowing, live beyond our means, but only for a limited period of time. Why should we think that collectively, as a nation, we are not bound by that same limitation?" -- Ronald Reagan
bdb@becker.UUCP (Bruce Becker) (01/12/90)
In article <1990Jan11.105904.16516@agate.berkeley.edu> gsmith@garnet.berkeley.edu (Gene W. Smith) writes: | | There has already been one request to get this crap out of |sci.math. Not only do you jerks not listen, this subject is still |cross-posted to a zillion other irrelevant groups. Put this |rubbish in comp.theory where it belongs, and try to remember that |not everyone on the net is a CS weenie. Hey! Watch your mouth! -- \\\\ Bruce Becker Toronto, Ont. w \66/ Internet: bdb@becker.UUCP, bruce@gpu.utcs.toronto.edu `/v/-e BitNet: BECKER@HUMBER.BITNET _< \_ "Head-slam me, Jesus, on the turnbuckle of life" - Godzibo
amull@Morgan.COM (Andrew P. Mullhaupt) (01/14/90)
In article <1990Jan11.105904.16516@agate.berkeley.edu>, gsmith@garnet.berkeley.edu (Gene W. Smith) writes: > > There has already been one request to get this crap out of > sci.math. Not only do you jerks not listen, this subject is still > cross-posted to a zillion other irrelevant groups. Put this > rubbish in comp.theory where it belongs, and try to remember that > not everyone on the net is a CS weenie. > -- This is a clear statement of your opinion; but why should I pay any attention to it? The subject in question is essentially mathematical, and is of interest in mathematics in its own right. Just because you aren't aware of this doesn't mean you can advertise your ignorance with impunity. One would naively expect that someone truly interested in mathematics would be interested in the question of the importance of proofs and their relative rigor in any subject. I would welcome any attempt you might mount to give an informed opinion regarding why proofs do not 'belong' in this or that subject or newsgroup. Later, Andrew Mullhaupt
cjs@bruce.OZ (Chris Stuart) (01/14/90)
In this discussion, it has been said that certain programs might resist proofs of correctness, because you can't solve the halting problem and thus there are programs for which you can't prove termination. However, the existence or difficulty of a proof of program "correctness" depends not only on the program, but also the definition of correctness. Consider a simple program that searches for positive integer solutions to x^n + y^n = z^n where x, y, z and n are all less that 2^20. (This may require handling integers which take up to 2.5M of storage each!). I can't prove whether or not this program will print out any solutions. (I am not a good enough mathematician to tackle Fermat's Last Theorem directly, and I don't have time to run the program to completion.) However, I can easily prove that the program will print out all solutions which do exist within the given range. For *any* program, there is always *something* that can be proven about it, even if you can't prove whether or not it terminates. In fact, there is nearly always something useful which can be proven. Cheers -- Christopher Stuart
park@usceast.UUCP (Kihong Park) (01/15/90)
In article <1788@bruce.OZ> cjs@bruce.OZ (Chris Stuart) writes: >In this discussion, it has been said that certain programs might resist >proofs of correctness, because you can't solve the halting problem and >thus there are programs for which you can't prove termination. If one is looking for a general correctness checker then this statement is true. But, in some instances(for whatever practical reason), one might restrict the domain of the checking algorithm to programs which fall into a well-defined subclass, e.g., the set of programs satisfying a certain structural form. For such special subclasses, each subclass may very well be a recursive set, hence the membership problem decidable.
gsmith@garnet.berkeley.edu (Gene W. Smith) (01/15/90)
In article <672@s5.Morgan.COM>, amull@Morgan (Andrew P. Mullhaupt) writes: >This is a clear statement of your opinion; but why should I pay >any attention to it? The subject in question is essentially >mathematical, and is of interest in mathematics in its own right. Asking whether, as a practical matter, proving correctness is a good programming technique is not a mathematical question. >Just because you aren't aware of this doesn't mean you can >advertise your ignorance with impunity. Just because you are a moron doesn't mean you should be obnoxious about it. >I would welcome any attempt you might mount to give an informed >opinion regarding why proofs do not 'belong' in this or that >subject or newsgroup. There *were* no proofs, jackass, there were a bunch of pointless arguments *about* proofs. Anyway, why cross-post to a zillion different groups? Pick one or two groups and pollute them, leaving the rest of us alone. -- ucbvax!garnet!gsmith Gene Ward Smith/Brahms Gang/Berkeley CA 94720 Fifty flippant frogs / Walked by on flippered feet And with their slime they made the time / Unnaturally fleet.
dwiggins@atsun.a-t.com (Don Dwiggins) (01/16/90)
I've read a few of the messages in this thread, and it triggered a question in my mind. Generally, in a mathematical theory, one doesn't construct proofs starting with the axioms if a reasonable set of useful theorems is available. In fact, when working in a new theory, the first order of business is to "build some tools" in the form of generally applicable theorems. Is there any work along those lines going on in the program verification field (e.g. something of the form "if the code of a loop matches pattern X, then it will satisfy invariants of the form Y"). Such theorems could be built into an automatic verifier and might cut the search space considerably. -- Don Dwiggins "Solvitur Ambulando" Ashton-Tate, Inc. dwiggins@ashtate.a-t.com
ladkin@icsib (Peter Ladkin) (01/18/90)
folks, i occassionally dream that those who post messages of content-free reaction are condemned to read news at 1200 baud. but then i wake up and realise, sadly, the world is not always the way we dream it. peter ladkin