Axioms

Of course, in "DeadMG++" then since you can deal with Expressions as raw semantic types, you can optimize them however you like. That means that we can introduce what's known as Axioms in the C++ world- as usual, a library-only feature.

Axioms are a simple concept. Consider

a = a + b; // 1
a += b; // 2

For most types, you would argue that (assuming the expression a is pure), the two are identical and an optimizing compiler might choose to change 1 into 2. Of course, for the remainder of types this would change the correctness of the program. Axioms are a system where you can tell "most" from "the remainder", allowing you implement very specific optimizations for UDTs which in C++ would be reserved for only primitive types. Pure helps with this at least a little, allowing us to apply CSE.

The main question is how would you design and specify Axioms?

At the most fundamental level, it would be a pair of expressions- transform one into the other for some benefit.

Axiom(
    Original := expr1 = expr1 + expr2,
    Preferred := expr1 += expr2
);

Axiom(
    Original := (expr1++).static_cast(void), // return value is unused
    Preferred := ++expr1
);

The question is, is that enough to implement all the Axioms that people might want, and is it implementable in such a relatively simple state?