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=-2.9 required=5.0 tests=BAYES_00,FREEMAIL_FROM, MAILING_LIST_MULTI autolearn=unavailable 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-12 18:20:16 PST Path: archiver1.google.com!news2.google.com!newsfeed2.dallas1.level3.net!news.level3.com!news-out.visi.com!petbe.visi.com!proxad.net!teaser.fr!enst.fr!melchior!cuivre.fr.eu.org!melchior.frmug.org!not-for-mail From: "amado.alves" Newsgroups: comp.lang.ada Subject: RE: Software Design Date: Sat, 13 Dec 2003 02:18:27 -0000 Organization: Cuivre, Argent, Or Message-ID: NNTP-Posting-Host: lovelace.ada-france.org Mime-Version: 1.0 Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: quoted-printable X-Trace: melchior.cuivre.fr.eu.org 1071281979 5132 80.67.180.195 (13 Dec 2003 02:19:39 GMT) X-Complaints-To: usenet@melchior.cuivre.fr.eu.org NNTP-Posting-Date: Sat, 13 Dec 2003 02:19:39 +0000 (UTC) To: Return-Path: X-MimeOLE: Produced By Microsoft Exchange V6.0.6487.1 content-class: urn:content-classes:message Thread-Topic: Software Design Thread-Index: AcPA6TDia7YQloN1RVW237nQC0gHbAAMiU1i X-OriginalArrivalTime: 13 Dec 2003 02:18:27.0955 (UTC) FILETIME=[65061430:01C3C11F] X-Virus-Scanned: by amavisd-new-20030616-p5 (Debian) at ada-france.org X-BeenThere: comp.lang.ada@ada-france.org X-Mailman-Version: 2.1.3 Precedence: list List-Id: Gateway to the comp.lang.ada Usenet newsgroup List-Unsubscribe: , List-Post: List-Help: List-Subscribe: , Xref: archiver1.google.com comp.lang.ada:3428 Date: 2003-12-13T02:18:27+00:00 << > "There are two ways of constructing a software design. One way is to > make it so simple that there are obviously no deficiencies. And the > other way is to make it so complicated that there are no obvious >deficiencies." C. A. R. Hoare It will be very interesting to see an operating system or at least a (visual) text editor, which has obviously no deficiencies, and at the same time is useful. I'd like to propose new term "hoareware" for the kind of software for which the quoted phrase is true. >> Cool name. But what's the denotation? I take it you mean (just) the = second sentence in Hoare's paragraph. The "correctness by construction" = series of papers by Peter Amey touch this (Google for it). Personally I = want to believe. 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. So in sum I think I agree with what I think you're = conjecturing: that for a piece of software to be useful it must be = complex by necessity. But the lesson from mathematics says a complex = thing can be shown correct. 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." =20 (Sorry if I sound rambling. I am :-) =20 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." =20