[OT] Identifying unused include directives?

[Robert Dewar]

> A way to avoid the undecidability, and that seems to be closer to what most
> programmers would view as the intuitive meaning, would be that the removal of
> the #include would not cause compilation errors or change the generated code.
> Normally we think of #include as being part of the *static* semantics.

Yes, that sounds like a reasonable definition, although the only practical
way of having the compiler test this would be to compile with and without
each #include.

Of course two #includes that were mutually dependent would not be caught
by this definition.