Jeffrey Yasskin <jyasskin_at_[hidden]> writes:

| 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.

That is *one* possible implementation.

You have to remember that the standards specification are
*specifications*, e.g. axiomatics in essence. Then a compiler has to
provide a definition. A compiler such as CompCert has to also
*prove* that the definition satisfies the specification.

(So the only time you get something wrong is when you have the wrong
translation from Standardese to Mathematics.)

| 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?

Why?

Remember that operator< on pointer has semantics implications more than
just being a (partial) order on pointers. It has ties to aliasing,
object extents, etc. An arbitrary ordeering such as std::less<T*> has
none of those additional constraints, which is why just because you can
define std::less<T*> means it is just as easy or even necessarily a good
idea to make operator< behave exactle the same.

-- Gaby