From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=0.1 required=5.0 tests=BAYES_05,INVALID_MSGID autolearn=no autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,86fd56abf3579c34 X-Google-Attributes: gid103376,public X-Google-Thread: 10db24,77f71d0bde4c5bb4 X-Google-Attributes: gid10db24,public From: cpp@netcom.com (Robin Rowe) Subject: Re: What good is halting prob? Date: 1995/04/20 Message-ID: #1/1 X-Deja-AN: 101283279 sender: cpp@netcom8.netcom.com references: <3kaksj$iur@isnews.calpoly.edu> <3mve9b$gaj@news.cais.com> <3n285v$9vl@news.cais.com> organization: NETCOM On-line Communication Services (408 261-4700 guest) newsgroups: comp.lang.ada,comp.edu Date: 1995-04-20T00:00:00+00:00 List-Id: To: crawford@cais2.cais.com (Randolph Crawford) Sb: Re: What good is halting prob? Randy, >You want a trivial correct program? > >main() >{ > if (1) exit( 0); >} > >It ain't much, but it's correct. Ok, here's the program's specification: "The program will report an error to the operating system on exit. An exit code of zero is not valid." Still think this code is correct? You might say this isn't fair, and I would agree. However, I think it illustrates my point that correctness is subjective. << If by correctness, you are thinking of "not incorrect", or "acceptably correct", there's a difference. >> I'm talking about proofs of correctness, where correctness is judged relative to a specification. << My point is, it's correct as long as it behaves entirely predictably (decidably). >> This is a very interesting definition. Most seem to feel that correctness is adherence to the specification. Given the combinatorial mathematics, correctness under your definition would seem to imply the halting problem. I guess I might as well give up my notion that the halting problem isn't useful. I've used it twice now in this thread. << Division by zero isn't important except as an exmple of failure. Likewise the inability to halt is a good example of failure. You can be certain of anticipating both of these failures *only* if your program is not a Universal Turing Machine. >> I can assure you that not one of my programs operates an infinite tape. ;-) << I think the blurring of the difference between software and bridges is where the confusion lies. No bridge can be proven correct. But it's traditional that the mathematical foundations used in building bridges *are* considered correct, ie. perfect. If a civil engineer found that error was cropping up in his computations *without his/her knowing* then any bridge or building he builds is at greater risk than he intended. >> If you mean that F=ma is the mathematical foundation then yes, that operates pretty well on bridges up to the speed of light. However, the state of the art is constantly improving in bridge modeling. After the LA quake, in which some bridges failed that shouldn't have, I recall a civil engineer quoted as saying they learn something new from every earthquake. The notorious Tacoma Narrows Galloping Gerty failure was due to a failure in the correctness of the mathematical model. Aerodynamic forces had not previously been considered. (Two earlier bridges failed for the same reason, but there wasn't any newsreel footage.) Engineers routinely build a safety factor into their designs in allowance for imperfections in the mathematical model. Except software engineers. Thanks for the feedback. Good points. Robin -- ----- Robin Rowe cpp@netcom.com 408-626-6646 Carmel, CA Rowe Technology C++ Design/Training Email for sample C++ Newsletter!