One could write axioms for types that don't have an operator==, or where comparison doesn't make sense: p=malloc(n) <=> p=realloc(0,n)
Wouldn't this mean the following? For any p and q of some type T:
p = malloc(n); q = realloc(0, n); assert( eq(p, q) );
Where eq() is the N3351 equality operator that checks if two objects are equal. eq could be implemented using == but it's more of a logical equality so even if a type doesn't have == than it is still logically sensible to check if two objects for that type are the same. In reality however, eq will have to be implemented and checkable somehow so if a type doesn't have a way to programatically checked for equality (using == or some other boolean function eq(), equal(), is_equal(), etc) then either you don't program the axiom or you add an assertion requirement to guard against the lack of == (like Boost.Contract does):
*cringe* Don't think about eq(). That was a compromise between myself and Marcin Zalewski. We couldn't determine if <=> should be interpreted as logical equivalence or behavioral equivalence (as in the previous axioms work). We ended assigning <=> to logical equivalence and using eq() as a kind of oracle that decided equality: either according to the rules of == or memberwise equality comparison. In retrospect, I think this was the wrong choice. Using <=> to describe the behavioral equivalence of two expressions provides a much more robust way of stating the relative meaning of operations. Andrew