Re: seperate keyword and seperate compilation with Gnat?

[bobduff@world.std.com (Robert A Duff)]

In article <JSA.96Jul11154350@organon.com>,
Jon S Anthony <jsa@organon.com> 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