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!aioe.org!.POSTED!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: Ada.Strings.Fixed.Count raises Storage_Error Date: Fri, 1 Jul 2016 15:08:23 +0200 Organization: Aioe.org NNTP Server Message-ID: References: <57346ac8$0$4570$426a74cc@news.free.fr> <57707888$0$5274$426a34cc@news.free.fr> <43a09f40-fdea-461e-9b0a-4419b86c1a56@googlegroups.com> NNTP-Posting-Host: vZYCW951TbFitc4GdEwQJg.user.gioia.aioe.org Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 8bit X-Complaints-To: abuse@aioe.org User-Agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:45.0) Gecko/20100101 Thunderbird/45.1.1 X-Notice: Filtered by postfilter v. 0.8.2 Xref: news.eternal-september.org comp.lang.ada:30993 Date: 2016-07-01T15:08:23+02:00 List-Id: On 01/07/2016 13:48, rieachus@comcast.net wrote: > On Wednesday, June 29, 2016 at 3:57:47 PM UTC-4, Dmitry A. Kazakov wrote: > >> Goedel results don't apply to programs anyway, because you are not >> required to decide anything using the program at hand. You are free to >> use *another* program, so you can break out. > > Sigh! Gödel proved not just that there are systems where some > functions cannot be computed correctly, but that there are functions > which cannot be computed correctly by any system. No. Goedel incompleteness does not mean that. Incompleteness is not transitive. If A is not provable in the formal system S that alone does not require it to be unprovable in Q. And, furthermore, completeness is not same as consistency (absence of paradoxes). Most of the statements are just not spellable in the formal system at hand. Nobody worries about that, after all, they were designed to prevent such statements to appear there. So, if the Liar's paradox were incomputable, who cares. > There are systems > which are not powerful enough to try to compute these functions, This is irrelevant. The behavior attributed to the bug of String index range is clearly: 1. Well-defined 2. Computable 3. Provable using very weak apparatus >> Nor the Halting problem does apply. For any program having a finite >> number of states, one clearly can decide in finite time with finite >> storage whether the program halts. > > Since when have Ada compilers dealt with only finite states?* They clearly do. Each Ada compiler has the upper limit of the program size it is capable to compile. Both the compiler and its outcome have a finite number of states. > * You may contend that your personal computer has a finite number of > states, but well before you can finish enumerating them, you will > upgrade the processor, memory, and/or disks (whether mechanical or solid > state). And then there are services like Drop Box which enable you to > store data "in the cloud." So the time when computers had a finite set > of states is long past. (Even Univac I, with 1000 words of memory, had > ten tape drives, and an operator to mount new tapes when required.) It does not matter, because you were arguing about *theoretical* undecidability, not about *practical* one. Theoretically it is clearly decidable and provable. Practicality is a whole different matter. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de