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=-0.3 required=5.0 tests=BAYES_00, REPLYTO_WITHOUT_TO_CC autolearn=no 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!.POSTED!not-for-mail From: "G.B." Newsgroups: comp.lang.ada Subject: Re: function Is_Open (File : File_Type) return Boolean; :Text_io Date: Fri, 30 Oct 2015 20:07:18 +0100 Organization: A noiseless patient Spider Message-ID: References: <87twpd2qlo.fsf@theworld.com> <1pj15r7pul7f1.15qgdyrc8k133$.dlg@40tude.net> <87pp0030c1.fsf@theworld.com> <135hiczk56x02.1xixcme8btbl4.dlg@40tude.net> <1dzlgoh4u2j7t$.1un3dfy0oeigd$.dlg@40tude.net> <190shqocxd87d$.1d68ghgqgbvfs$.dlg@40tude.net> <19ihs115mzocg$.20s63jo0q2gf.dlg@40tude.net> <2qwfwnugm5q5.ajan0n5midql$.dlg@40tude.net> <18wdhboc0r4aj$.1rj6n8wv3scfd.dlg@40tude.net> Reply-To: nonlegitur@futureapps.de Mime-Version: 1.0 Content-Type: text/plain; charset=windows-1252; format=flowed Content-Transfer-Encoding: 7bit Injection-Date: Fri, 30 Oct 2015 19:05:06 -0000 (UTC) Injection-Info: mx02.eternal-september.org; posting-host="b96887e80893c84a90c3007226ca0d1c"; logging-data="9420"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX19W42VMSDnfyWHrgmgKnwmNAff3zmxbBo4=" User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.10; rv:38.0) Gecko/20100101 Thunderbird/38.3.0 In-Reply-To: <18wdhboc0r4aj$.1rj6n8wv3scfd.dlg@40tude.net> Cancel-Lock: sha1:sN6OwQC+Oe3PwnEXsuQf0TmPYbY= Xref: news.eternal-september.org comp.lang.ada:28142 Date: 2015-10-30T20:07:18+01:00 List-Id: On 30.10.15 17:20, Dmitry A. Kazakov wrote: > On Fri, 30 Oct 2015 15:32:16 +0100, G.B. wrote: > >> On 30.10.15 09:39, Dmitry A. Kazakov wrote: >>> The concern is safe design. If [program] B has bugs it cannot be >>> relied on to determine if it has them. >> >> Uhm, so what? Which kind of program is relied upon to determine >> if it has bugs or not? > > A program that contains run-time checks for bugs. I don't think anybody says that, nor does "contract based design", not the part with "relying"! As is apparent from the Ada Rationale ("for debugging..."). As was apparent from some quoted paragraphs. Also of interest is Hoare's idea of a SIMPLYFYING_ASSUMTION. Which is to be used in some situations(!), but not in others. >> OTOH, what if we can learn about potential bugs because we happen >> to think that a failed expression has exactly that potential >> for us? > > What kinds of answer do you expect? If someone is assuming that programmers will always start their thinking from something comprehensively correct, I expect his answer to reflect this. In other cases, the ones I consider more ordinary, decent programming, I'd expect this: "... needs to be assessed empirically." > Positive of *what*? Positive of what we now have learned may (not) be the desired outcome. In some cases, that's too late. In many cases, we stop before rollout. We might be stymied. > You first need a workable (...) definition of a correct > program What makes you assume that a specific, formalistic definition of a correct program is the workable one? Except per the narrow situation-excluding circularity of "work" = "operation": Considering the most successful software companies on this planet, while they do not profit from selling correct (formally, somehow) programs(*), they still strive for local correctness. (A program that was correct for Ariane IV was not correct(?) for ... Again, situations!) So, I guess, one might poke fun at tests that make test runs of programs fail because the test was failing, one might start from world-excluding definitions that of necessity produce a contradiction, or one might make jokes about programming efforts that assume that sufficient formalization is possible. All are justified, IMHO. __ (*) Since, who would pay for updates?