Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!think.com!mintaka!bloom-beacon!eru!hagbard!sunic!mcsun!corton!ilog!barbes!davis From: davis@barbes.ilog.fr (Harley Davis) Newsgroups: comp.lang.misc Subject: Re: Formal definitions (Re: ada-c++ productivity) Message-ID: Date: 22 Apr 91 16:09:40 GMT References: <1726@optima.cs.arizona.edu> <29344@dime.cs.umass.edu> <12297@dog.ee.lbl.gov> <11204@uwm.edu> Sender: davis@ilog.fr Organization: ILOG S.A., Gentilly, France Lines: 23 In-reply-to: markh@csd4.csd.uwm.edu's message of 20 Apr 91 04:08:58 GMT In article <11204@uwm.edu> markh@csd4.csd.uwm.edu (Mark William Hopkins) writes: If it's proven mathematically, it *will* work. And if it doesn't, then it's provably the fault of the underlying hardware (or compiler or assembler). And yes, I've run into these conditions countless number of times already. But the point is, after verification, responsibility for proper functioning is no longer the software writer's job. That job is complete. Software is valid, even when it does not function normally due to faulty hardware or translators. Sadly, for those of us who are paid to deliver working software, this is not true. The software has to work despite flaky hardware or underlying levels which do not meet their (often poorly) documented interfaces. -- Harley Davis -- ------------------------------------------------------------------------------ nom: Harley Davis ILOG S.A. net: davis@ilog.fr 2 Avenue Gallie'ni, BP 85 tel: (33 1) 46 63 66 66 94253 Gentilly Cedex, France