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=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,8a63984119013357 X-Google-Attributes: gid103376,public X-Google-ArrivalTime: 2003-12-13 05:40:49 PST Path: archiver1.google.com!news2.google.com!newsfeed2.dallas1.level3.net!news.level3.com!zeus.visi.com!news-out.visi.com!green.octanews.net!news.octanews.net!news-xfer.cox.net!peer01.cox.net!cox.net!news-hub.cableinet.net!blueyonder!internal-news-hub.cableinet.net!news-text.cableinet.net!53ab2750!not-for-mail User-Agent: Microsoft-Entourage/10.1.4.030702.0 Subject: Re: Software Design From: "(see below)" Newsgroups: comp.lang.ada Message-ID: References: Mime-version: 1.0 Content-Type: text/plain; charset="US-ASCII" Content-transfer-encoding: 7bit Date: Sat, 13 Dec 2003 13:40:48 GMT NNTP-Posting-Host: 82.41.186.221 X-Complaints-To: abuse@blueyonder.co.uk X-Trace: news-text.cableinet.net 1071322848 82.41.186.221 (Sat, 13 Dec 2003 13:40:48 GMT) NNTP-Posting-Date: Sat, 13 Dec 2003 13:40:48 GMT Organization: blueyonder (post doesn't reflect views of blueyonder) Xref: archiver1.google.com comp.lang.ada:3437 Date: 2003-12-13T13:40:48+00:00 List-Id: On 13/12/03 2:18 am, in article mailman.109.1071281924.31149.comp.lang.ada@ada-france.org, "amado.alves" wrote: > And I ponder this evidence from mathematics: that really very *complex* proofs > are found flawless, i.e. absolutely correct, e.g. (the proofs of) Fermat's > Last Theorem, the Four Coulor Theorem. But the Wiles proof of FLT was found to be erroneous shortly after after publication. It has since been "debugged". Its present status is a matter of the opinion of the mathematicians who participated in that effort, as far as I can see. The 4CT was greeted with outright scepticism when announced. I do not know what has happened since to confer "absolutely correct" credentials. > a piece of software to be useful it must be complex by necessity Agreed. > But the lesson from mathematics says a complex thing can be shown correct. I think this is highly questionable. Moreover, it is the proofs (metaphorically, the programs) that are complex in the examples above. The theorems (metaphorically, the specifications) are (very!) simply stated. Software contends with complex, ill-defined and time-varying requirements and specifications in a way that does not arise with these famous theorems. > That is, what we need is not simple: it's a way to show (and experience) > the complex correct. In a way, anti-Hoare. You know, "0% bugs." Absolutely, yes. But the big problem, for software, is to know what standard of correctness to hold the program to. > The one piece of complex software in the world that is flawless is perhaps > TeX. But it took decades to show that. Not satisfactory. I dream of complex > programs being proved correct just like complex mathematical proofs: by > revision. Clearly one way to accomplish this is to write them in a rigourous > and readable language and of course in very good style. Hence "100% Ada." Well, people tried and failed to prove the 4CT & FLT for hundreds of years. 8-) -- Bill:Findlay chez Blue:Yonder dot:co:dot:uk (":" => "")