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!feeder.eternal-september.org!aioe.org!.POSTED!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: "functional" programming in Ada Date: Fri, 9 Mar 2018 09:38:23 +0100 Organization: Aioe.org NNTP Server Message-ID: References: <896b83c6-83d4-4ffc-8c56-1481802ea8fd@googlegroups.com> <961c82e0-7d7e-48af-8751-916a3332ccc5@googlegroups.com> <1520428274.2488.155.camel@obry.net> NNTP-Posting-Host: MyFhHs417jM9AgzRpXn7yg.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:52.0) Gecko/20100101 Thunderbird/52.6.0 X-Notice: Filtered by postfilter v. 0.8.3 Content-Language: en-US Xref: reader02.eternal-september.org comp.lang.ada:50905 Date: 2018-03-09T09:38:23+01:00 List-Id: On 08/03/2018 23:49, G. B. wrote: > Dmitry A. Kazakov wrote: >> On 08/03/2018 04:34, Randy Brukardt wrote: >>> The various contracts (preconditions, postconditions, predicates, etc.) all >>> contain some executable code, and it is necessary for callers to be able to >>> understand those contracts. Expression functions help in this, while the >>> bulk of the implementation should remain in the body. >> >> These are not contracts if have any executable code, and more >> importantly, understanding cannot be achieved by exposing >> implementation/code. >> >> P.S. Contracts exist prior the program (programs, actuall) and surely >> prior to any execution of (any implementation of any programs under the >> contract). >> > > If there is nothing that ever assigns a value to a contract’s > clause, then there id none. So, in order make it something, > an evaluation of clauses needs to be performed. Somewhere, > somehow. My brain is operating when doing this, or so I hope, > and whenever it does following discipline, then it is executing > a program. > > The troublesome idea is to think that the program > and its contract are like “x ε x”, or like recursive types. Yes, unless the types algebra is clearly separated from the language enough for the recursion to start and end before it comes to any use of the type. Anyway, since type contracts are most important ones, it is difficult to accept recursive definitions of types (as well as pattern matched types or templates beyond trivial) because they make it for the reader to understand the meaning of the contract. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de