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!news.eternal-september.org!feeder.eternal-september.org!aioe.org!.POSTED!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: Ada 2012 Constraints (WRT an Ada IR) Date: Sat, 3 Dec 2016 11:23:17 +0100 Organization: Aioe.org NNTP Server Message-ID: References: <92ed75e9-baae-455c-9e34-53348dc6eaef@googlegroups.com> <03847fd7-5699-48de-bb3c-ef5512398f26@googlegroups.com> <3ef819e8-55f7-4ef7-9f37-77e6abc33f98@googlegroups.com> NNTP-Posting-Host: s3c6wwRqkurrfTZpuYYZ+w.user.gioia.aioe.org Mime-Version: 1.0 Content-Type: text/plain; charset=windows-1252; format=flowed Content-Transfer-Encoding: 7bit X-Complaints-To: abuse@aioe.org User-Agent: Mozilla/5.0 (Windows NT 10.0; WOW64; rv:45.0) Gecko/20100101 Thunderbird/45.5.1 X-Notice: Filtered by postfilter v. 0.8.2 X-Mozilla-News-Host: news://news.aioe.org Xref: news.eternal-september.org comp.lang.ada:32584 Date: 2016-12-03T11:23:17+01:00 List-Id: On 2016-12-02 20:50, G.B. wrote: > On 02.12.16 17:21, Dmitry A. Kazakov wrote: >> Predicates are just arbitrary expressions the programmer sets without >> understanding all effects of his actions. > > So are programs. When written in C? > While I think I understand the desire for a fully proven > type centered, consistent, awesome Ada program and supporting > language, meanwhile a simple > > pragma Assert (Is_Sorted (S)); -- S a library level constant > > has in effect created a desirable change in behavior of an > older program here. Even though the behavior so far had not > caused any concern, a bug was sure lurking. That is exactly the point. You falsely assume that the effect of run-time assertion fault would be better than the effect of potential bug in any given context. When swapping one bug for another you still have it, and as with all bugs, the effect is not to predict. > It's programmers who write programs, improving their understanding > of a lot of thing that affects their programs, using assertions. and tracing and tests... > Now, do assertion distract from learning how to write correct > programs using types that manage to express them? Yes they do. It has nothing to do with correct programs, as you change one bug for another. > And in such > a way that an Ada compiler can determine truth at compile time? This is not how predicates work and has nothing to do with truth. The only truth about a program is whether it exposes predefined behavior. The main objection to arbitrary predicates is that they expose an undefined, undecidable, unexpected, undesired behavior. It is all a decent software design technique is against. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de