RE: [boost] metactrl header [compile time asserts]

From: Borgerding, Mark A. (MarkAB_at_[hidden])
Date: 2000-07-28 09:18:44

A postulate is the basic foundation upon which a mathematical proof is
built.  If the postulate is incorrect then a proof that assumes it may not
be correct.  I think this is a close analogy to a computer program.  If the
basic assumptions of the program's author are not met, then the program may
not operate correctly.

I agree with the need of simplicity in the assumptions.  It is very easy for
a code's author to comment that a function will only work on big endian
machines.  This is a basic assumption and is so simple it is not questioned
for a given domain.  The concept of domain being key here.

The target platform of the program makes up the domain for the compile-time
postulate.
For a given platform, the postulate will always be strictly true, or false.

A mathematical example:
postulate: "Any number must be greater than, equal to, or less than zero."
This postulate is quite reasonable and is in fact used as the basis for
mathematical, but the domain is limited to real numbers.  A couple of
attempts to prove Fermat's last conjecture were foiled because they
attempted to use this postulate in the domain of complex numbers.

I am not suggesting that a programmer would be able to apply the same
scrutiny and rigor to a piece of code as a mathematician does to a proof.
If the code is laid out thoughtfully, then the successful compilation of the
program could be considered analogous to a mathematical proof, with most
assumptions checked at compile time.  However, there are generally very
basic concepts that we assume when programming: the computer will not lose
power, memory will not have bit errors, filesystems will not be corrupted.
We make these assumptions, not because they are obviously true, but because
without assuming *something*, we cannot make functional programs.  Even if I
were to write a program that checked a filesystem's integrity, I would
probably need to assume the memory in the computer was reliable.

> -----Original Message-----
> From: David Abrahams [mailto:abrahams_at_[hidden]]
> Sent: Friday, July 28, 2000 9:38 AM
> To: boost_at_[hidden]
> Subject: Re: [boost] metactrl header [compile time asserts]
> 
> 
> 
> ----- Original Message -----
> From: "Borgerding, Mark A." <MarkAB_at_[hidden]>
> 
> 
> > According to Webster:
> > postulate:
> > Function: transitive verb
> > 1 : DEMAND, CLAIM
> > 2 a : to assume or claim as true, existent, or necessary :
> > depend upon or start from the postulate of b : to assume as 
> a postulate or
> > axiom (as in logic or mathematics)
> > Function: noun
> > 1 : a hypothesis advanced as an essential presupposition,
> > condition, or premise of a train of reasoning
> > 2 : AXIOM 3
> >
> >
> > Along those lines, I also like any of these forms:
> >
> > AXIOM( sizeof(int == 4 );
> > DEMAND( sizeof(int) == 4 );
> > PREMISE( sizeof(int) == 4 );
> 
> Ah, but that's exactly why postulate is the wrong word. To postulate
> something means to offer it as a premise without proof. Any 
> logical system
> depends on some truths which cannot be proven (read:
> "checked") inside the system (Godel, said that, I think). I 
> think the point
> of an axiom is to make your assumptions so simple on the face 
> of it that
> even skeptics are willing to concede them. But our 
> compile-time assert is
> inherently provable, or there would be no point in writing it!
> 
> -Dave
> 
> P.S. I like COMPILE_TIME_ASSERT
> 
> 
> 
> 
> --------------------------------------------------------------
> ------<e|-
> Download iPlanet Web Server, FastTrack Edition 4.1 for FREE,
> and start publishing dynamic web pages today!
> http://click.egroups.com/1/7540/4/_/9351/_/964791174/
> --------------------------------------------------------------
> ------|e>-
> 
> 
>