Blaisorblade0

> I have never run across anyone with legal training using "spirit" language.

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

Throwing away large chunks of code is what optimizers exist for! Sadly, most discussions of UB only show when it "goes wrong" (has surprising results), not when it goes right!

@ceilingcorner's main point is that, no matter how healthy you live, an obese person is more likely to infect you. I don't know if I buy that, but I agree none of your answers seem to be on point.

Great example, can I please borrow that? Is a link sufficient attribution?

Why don’t they just disable optimizations then? I think that’s because they also want performance, even when it requires pointers to not be just addresses.

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 you can’t compare to the concrete model, because it’s not the status quo. That ship already sailed with C89 and strict aliasing. Ptr2int casts were never legal, and support was inconsistent.

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

First, this change is reducing undefined behavior* (EDIT: see below), and that undefined behavior (most casts between pointers and integers) did _not_ work reliably in practice. And in fact, the semantics they chose is rather sensible.

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.

> Some professionally oppressed people contact a project, provide mostly secret evidence to members of the project's progressive faction.

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

Coq’s name _was_ meant to be offensive to English speakers. And the team does want to avoid names that are offensive in other languages, as EVERYBODY does when choosing international brand names.

We _know_ it doesn’t just come from Coquand’s name, because Gérard Huet very clearly said so.

The thread is full of stories like “woman says she works on Coq and gets harassed” or “woman foresees this problem and avoids learning Coq” or “Coq teacher (male or female) struggles to talk about Coq because students are uncomfortable”.

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.