On Tue, Aug 27, 2013 at 10:28 AM, Xavier Leroy <Xavier.Leroy_at_[hidden]> wrote:
> On 27/08/13 17:48, Jeffrey Yasskin wrote:
>>> - As a semanticist, I think it would be challenging to formalize, for
>>> the general reasons given above.
>>
>> How do you model std::less<T*>, which already requires this total but
>> unspecified order?
>
> No one tried, as far as I know. We (as a community) are still a long
> way from formalizing the complete semantics of a "big" language like
> C++, but an even longer way from formalizing specs for its standard
> library...
>
> There are plausible ways to formalize this total order at the source
> language level. But, as Gabriel wrote, the difficulty is to ensure
> that your source-level semantics is not making predictions that the
> compiler could invalidate later.
>
> In other words: at the end of the day, your pointers are just bit
> patterns that the hardware compares as if they were integers. If you
> could chase this hardware ordering of pointers back every compilation
> pass, it should be the case that the source-level ordering you obtain
> is one of those allowed by your source-level semantics. Proving this
> kind of properties sounds very challenging to me.

Mhmm. It sounds like you probably can't model the
implementation-defined conversion to intptr_t yet either? Since
T*->intptr_t->T* has to be an identity map, and intptr_t is totally
ordered.

If that's the case, it sounds like making operator< on T* a total
order would reduce the fraction of C++ that's currently formalizable
but wouldn't make it any harder to formalize the whole language?