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,6a9844368dd0a842 X-Google-Attributes: gid103376,public From: bobduff@world.std.com (Robert A Duff) Subject: Re: seperate keyword and seperate compilation with Gnat? Date: 1996/07/11 Message-ID: #1/1 X-Deja-AN: 167864768 references: <31D95D93.28D8D15B@jinx.sckans.edu> organization: The World Public Access UNIX, Brookline, MA newsgroups: comp.lang.ada Date: 1996-07-11T00:00:00+00:00 List-Id: In article , Jon S Anthony wrote: >Well here we just plain disagree. In fact, this statement is >positively wog-boggling. Using your apparent "criteria" here, you >would have to say that the statement of any theorems in a mathematical >treatise are somehow counter to the precision and clarity of >exposition of the material. They are clearly "redundant" in the >strictly formal sense, i.e., they are deducible from the definitions, >axioms (and perhaps various meta information - interpretations, models >and whatnot). But those math textbooks always label those as "theorems", to make it clear that these are not axioms, but can be derived. And they usually show the proof, or an outline of the proof. Or they "exercise the interested student". ;-) The rules of the RM proper are entirely definitions and axioms. Anything that's a theorem is put in a NOTE, so you know it's not a basic fact, but can be derived from other facts. So, I would have strongly objected to your suggestion as an RM rule, but I would have considered it as a NOTE. For a NOTE (as for a theorem in a math text), you include it if it seems interesting enough, and doesn't make the book too big, and so forth. All highly subjective considerations. Lots of people suggested lots of NOTES, and it was always a judgement call as to whether that particular fact was interesting enough to the general reader. There's always Ada textbooks, which have lots more theorems than the RM. >Highly precise and formal works (more formal and precise than the RM >was ever dreamed to be in the wildest fantasies of those involved) are >absolutely _FULL_ of this sort of "redundancy". In fact, it is a >hallmark of such works. True, but they always make a clear distinction between basic facts (axioms) and interesting redundant facts (theorems). >the RM as written is good enough. Nice to know. ;-) - Bob