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.3 required=5.0 tests=BAYES_00,INVALID_MSGID autolearn=no autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,611f4b10cbf9af69 X-Google-Attributes: gid103376,public From: Robb Nebbe Subject: Re: Redefinition of Equality (Long) Date: 1996/10/02 Message-ID: <32525C08.5C77@iam.unibe.ch>#1/1 X-Deja-AN: 186673125 references: <52hgmoINN7tg@snoopy.cis.ohio-state.edu> <324FD267.954@cis.ohio-state.edu> content-type: text/plain; charset=us-ascii organization: Dept. of CS, University of Berne, Switzerland mime-version: 1.0 newsgroups: comp.lang.ada x-mailer: Mozilla 2.02 (X11; I; SunOS 5.4 sun4m) Date: 1996-10-02T00:00:00+00:00 List-Id: Robert A Duff wrote: > Well, the goal is to make sure that the compiler can *check* that the > abstract value of an 'in' parameter is not modified. > ... And any time you > want to check things at compile time, you have to put up with rules that > are more pessimistic than they might be. In this particular case you may be right but I wouldn't expect this to be true in general. I am sort of plucking this out of context but I have seen other people say similar things. There is nothing intrinsic in compile time checking of semantic properties that makes it necessarily pessimistic. In terms of model theory (the branch of metamathematics that deal with these kinds of issues) your statement is the equivalent of saying that no logic (think logical system) can ever be both sound (~safe) and complete (~not pessimistic) which is known to be false. In a real language it might be the case that something isn't decidable in which case you must choose to err on the side of safety or expressiveness with dynamic checks to compensate. Or it might be possible but just too complicated to be worth the effort. Or it just might be that it isn't currently known how to do the checks. Robb Nebbe