I know what you mean (and agree), but some spirit language seems required by the subject matter :-)...

I'm familiar with https://coq.discourse.group/t/alpha-announcement-coq-is-a-le..., which was just hard, but it does not prove Lean consistent, it only lets Coq process the Lean stdlib.

https://en.wikipedia.org/wiki/Computer_Modern#Latin_Modern

From N2176, Sec. 6.3.2.3, p. 5-6: > An integer may be converted to any pointer type. Except as previously specified, the result is implementation-defined, might not be correctly aligned, might not point to an entity of the referenced type, and might be a trap representation.

> Any pointer type may be converted to an integer type. Except as previously specified, the result is implementation-defined. If the result cannot be represented in the integer type, the behavior is undefined. The result need not be in the range of values of any integer type.

AFAICT, that doesn’t even guarantee that a roundtrip is the identity — which C++ mandates and is still the case: http://eel.is/c++draft/expr.reinterpret.cast#5

EDIT: GCC does have those restrictions in place already: https://gcc.gnu.org/onlinedocs/gcc-11.1.0/gcc/Arrays-and-poi...

and since a while (earliest relevant docs I could find easily): https://gcc.gnu.org/onlinedocs/gcc-3.1.1/gcc/Arrays-and-poin...

EDIT2: LLVM doesn’t document this “implementation-defined behavior” (or most others), even if docs are explicitly required by the standard; but it does use pointer provenance in practice already, but not in a way that’s easy to explain.

And pointers weren’t addresses before either. My favorite example of “pointers aren’t addresses” is this kind of code:

int a[…]; int b[…]; /* … */ a[i] = 0; b[j] = 1; return a[i];

Ignoring this discussion for a moment, wouldn’t you expect `return a[i];` to optimize to `return 0;` here? After all, `a` and `b` are disjoint arrays! I’m sure many would be disappointed if the compiler did not do that optimization, right?

But kudos for finding an official source of misinformation.

What’s more, the committee already gave license to implementations to be “overzealous”, as you call them. That did contradict the standard, but they never bothered to fix it.

So it’s not the first time the C committee contradicts itself and doesn’t bother to resolve the contradiction. So yes, you’re entitled to feel you’ve been lied to before, they’re just being honest now.

GCC has been using http://www.open-std.org/jtc1/sc22/wg14/www/docs/dr_260.htm to justify its use of provenance, even when it contradicts the standard.

For instance, GCC sometimes tracks pointer provenance through integers; this proposed change will make that clearly illegal.

But yes, some code with UB which works for now might break. But that’s true whenever you upgrade your C compiler or use optimizations, so for correctness you shouldn’t do either! People working on certified embedded software have known that for long.

The real problem is that C users have been lied to. They’ve been taught the lie that C pointers are just addresses, that memory is an array of bytes, that relying on this lie is robust, and that this combination is fast. But this combination is impossible.

EDIT: officially some behavior was implementation-defined, but implementations made it undefined anyway — either officially or via bugs; links in subthread.

> After the re-naming they are never heard of again.

Beyond all other corrections, the people complaining here are professional Coq users of both genders.

You seem to suggest those people train everybody around them to change behavior.

Meanwhile, every company picking a brand name will do the smart thing and avoid anything ridiculous in any of their target market; yet somehow if this happens in public it’s a scandal.

But generally, algorithms researchers seem to not care about abstractions, as witnessed by TeX and LaTeX in multiple ways.

That's probably because when you really need to invent a fancy algorithm (which is their job), that will often not be built out of reusable components.

Regarding compatibility: neither Coq nor Agda used to have much of it; nowadays Coq is maintained together with a large set of community projects, and code is much more stable. Still tons to do.