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: f891f,9d58048b8113c00f X-Google-Attributes: gidf891f,public X-Google-Thread: 101deb,b20bb06b63f6e65 X-Google-Attributes: gid101deb,public X-Google-Thread: 1014db,9d58048b8113c00f X-Google-Attributes: gid1014db,public X-Google-Thread: 103376,2e71cf22768a124d X-Google-Attributes: gid103376,public X-Google-Thread: 10cc59,9d58048b8113c00f X-Google-Attributes: gid10cc59,public From: dewar@cs.nyu.edu (Robert Dewar) Subject: Re: next "big" language?? (disagree) Date: 1996/06/18 Message-ID: #1/1 X-Deja-AN: 161541346 references: <4p1l65$35qi@info4.rus.uni-stuttgart.de> <4p60nk$imd@euas20.eua.ericsson.se> <4p8lmq$oq7@goanna.cs.rmit.edu.au> <4pj8p7$h9r@goanna.cs.rmit.EDU.AU> organization: Courant Institute of Mathematical Sciences newsgroups: comp.lang.pascal,comp.lang.c,comp.lang.misc,comp.lang.pl1,comp.lang.ada Date: 1996-06-18T00:00:00+00:00 List-Id: A. Grant asks "Why don't you like assertions enabling optimisation where the compiler can prove the correctness of the assertion, i.e. optimise it away? Then all you are doing is giving a hint to the compiler about an optimisation strategy, without altering the meaning of the program at all." There is nothing wrong with such assertions (they are typically called pragmas in Ada for example), but they are TOTALLY different from the kind of assertions that people want for debugging code. Both uses are perfectly valid, but quite incompatible semantically, and part of the trouble in designing facilities in languages for assertions is that these two uses get badly entangled, both at the informal discussion level, and at the formal semantic description level. Actually there are many shades here. FOr example, to some people, assertions are things the compiler can trust regardless of proof (some of the pragmas in Ada are like this too). To others, they require proof as yu suggest and are merely hints to enable otherwise allowed transformtaions of the code, to others they are debuging statements to be executed at run time etc. etc.