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=unavailable autolearn_force=no version=3.4.4 Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!mx02.eternal-september.org!feeder.eternal-september.org!news.albasani.net!fu-berlin.de!uni-berlin.de!individual.net!not-for-mail From: Niklas Holsti Newsgroups: comp.lang.ada Subject: Re: Ada.Strings.Fixed.Count raises Storage_Error Date: Wed, 29 Jun 2016 21:49:49 +0300 Organization: Tidorum Ltd Message-ID: References: <57346ac8$0$4570$426a74cc@news.free.fr> <57707888$0$5274$426a34cc@news.free.fr> <43a09f40-fdea-461e-9b0a-4419b86c1a56@googlegroups.com> Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 8bit X-Trace: individual.net mLeP2c2f4gf33T0gPVXQ+ApRkBNUHBEYFAiiVRiJMTsVcKT6YW Cancel-Lock: sha1:m6Wy08KaMb0QCKcSAxNhU56dvMA= User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.8; rv:45.0) Gecko/20100101 Thunderbird/45.1.1 In-Reply-To: <43a09f40-fdea-461e-9b0a-4419b86c1a56@googlegroups.com> Xref: news.eternal-september.org comp.lang.ada:30972 Date: 2016-06-29T21:49:49+03:00 List-Id: On 16-06-27 07:48 , rieachus@comcast.net wrote: > On Sunday, June 26, 2016 at 8:51:21 PM UTC-4, Xavier Petit wrote: > >> Every parameters of a subprogram should be anticipated and produce >> a coherent behavior. It’s hard but Ada is especially here to make >> it easier. > > Gödel, Escher, Bach: An Eternal Golden Braid, is a 1979 book by > Douglas Hofstadter that is now in its 20th edition. > > It tries, among other things to explain the reality revealed by > Gödel's proofs. One of those consequences is that you can't build a > perfect compiler. That depends on what you mean by a "perfect" compiler. Please explain. > In fact, the gnat in Ada Core Technologies logo is > a cute reminder that every compiler must have at least one bug. I do not believe that statement. It would mean that efforts to produce verified compilers, for example CompCert (http://compcert.inria.fr/index.html), are fundamentally misguided. > Worse, the Halting Problem is a very simple proof that you cannot > write a program that will perfectly determine whether a given > software program will halt. (Or not halt, if you work on embedded > systems like I did.) What has that do with the issue? Yes, there is no algorithm that can determine if any given program halts or not. Nevertheless, there are plenty of programs for which termination, or non-termination, can be proved and has been proved. And one of the skills required of a programmer is to write programs (compilers or applications) that terminate when required, or that keep running forever if that is required, and to present argument or proof that the program indeed has the desired behaviour. > So trying for perfection in compilers, programming languages, and > even many software programs is a mug's game. You can't do it, you > don't know where other corner cases are, and you can't even document > all of the bugs. Yes, it is possible to "prove" software correctness > for some programs. But for those same programs, you have just moved > the target, from perfect software to perfect requirements. Oh, that old argument. Yes, requirements are human creations, and therefore informal at source. Nevertheless, there are many methods to examine, review, verify, and validate requirements, both informal and formal ones. They are not perfect, but are often useful. An analogous argument is that if a bridge is required to carry a load of 100 tons, the engineers do not have to make any analysis to determine how thick the pillars should be, because perhaps the requirement is in error, and the real requirement is 80 tons, or 150 tons, or something else, so there is no point in trying to prove that the design will carry 100 tons. Silly. I'm astonished that you seem to be saying that Gödel's results mean that this clear and simple bug in a library function should not be reported to AdaCore. Really. Perhaps you are afraid that this is the last bug in GNAT, and as you believe that every compiler must have at least one bug, removing this bug would mean that GNAT would no longer be a compiler :-) -- Niklas Holsti Tidorum Ltd niklas holsti tidorum fi . @ .