Re: "functional" programming in Ada

[G. B. <nonlegitur@nmhp.invalid>]

Dmitry A. Kazakov <mailbox@dmitry-kazakov.de> 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.