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,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-13 14:09:09 PST Path: archiver1.google.com!news2.google.com!newsfeed2.dallas1.level3.net!news.level3.com!crtntx1-snh1.gtei.net!washdc3-snh1.gtei.net!news.gtei.net!ngpeer.news.aol.com!feed2.newsreader.com!newsreader.com!news2.telebyte.nl!news.completel.fr!blob.linuxfr.org!213.91.2.137!teaser.fr!enst.fr!melchior!cuivre.fr.eu.org!melchior.frmug.org!not-for-mail From: "Alexandre E. Kopilovitch" Newsgroups: comp.lang.ada Subject: RE: Software Design Date: Sun, 14 Dec 2003 00:22:22 +0300 (MSK) Organization: Cuivre, Argent, Or Message-ID: References: <468D78E4EE5C6A4093A4C00F29DF513D04B82AFF@VS2.hdi.tvcabo> NNTP-Posting-Host: lovelace.ada-france.org Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Trace: melchior.cuivre.fr.eu.org 1071353182 66006 80.67.180.195 (13 Dec 2003 22:06:22 GMT) X-Complaints-To: usenet@melchior.cuivre.fr.eu.org NNTP-Posting-Date: Sat, 13 Dec 2003 22:06:22 +0000 (UTC) To: comp.lang.ada@ada-france.org Return-Path: In-Reply-To: <468D78E4EE5C6A4093A4C00F29DF513D04B82AFF@VS2.hdi.tvcabo>; from "amado.alves" at Sat, 13 Dec 2003 02:18:27 -0000 X-Mailer: Mail/@ [v2.44 MSDOS] 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:3449 Date: 2003-12-14T00:22:22+03:00 amado.alves wrote: >I dream of complex programs >being proved correct just like complex mathematical proofs: by revision. There is a common misconception (among non-mathematicians) about the nature and power of mathematical proofs: those proofs do not signify for a final and eternal truth as many non-mathematicians believe; a proof just exposes a logic which leads to the theorem's conclusion. So anyone who relies upon a theorem is supposed to check and agree with that logic. Because of that, too complex proofs have less value in mathematics then simple proofs (too few people can actually inspect the logic of, say, 100-page highly demanding mathematical text), and therefore inventing of a new, simple and straightforward proof for already proven (but only by lengthy and complex proof) theorem is always regarded as quite respectable mathematical result. > 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." Obviuosly, the language, terminology and notation used in a proof greatly influences reader's ability to inspect its logic. A clear language, well-chosen and stable terminology and notation are if fact prerequisites for wide and effective use of a mathematical result. In this sense Ada language is certainly on right way - Ada strives to provide exactly that - clear, well-chosen and stable notation as well as basic level of the language for programs/software, and a good exposition of a logic and intentions is a highly useful thing even if it is somehow incomplete and/or unpolished regarding to mathematical standards. But anyway, what should be never forgotten - equally in software engineering and in mathematical applications - that both ends of a proved thing must be checked every time: that actual prerequisites are strong enough for the proof to be applicable and that the theorem's conclusion is enough to satisfy actual requirements. And this is the most critical point in usage of "already proved" things. Alexander Kopilovitch aek@vib.usr.pu.ru Saint-Petersburg Russia