Abstract interpretation is also at the heart of Julia’s type inference algorithm (amongst other analyses that Julia performs)
A very useful framework, both practically and theoretically!
I don't want an optimizer that eliminates an unnecessary operation. I want a compiler that tells me that it is unnecessary so I can remove it.
This is operating on IR, not on lines of code. Figuring out where the operation came from is extremely difficult because you have to propagate all of that info back and forth across the passes, and it may end up being split "across" syntactic elements. If your language has any form of metaprogramming or code reuse (i.e. all of them), that operation may also be necessary at some use sites and not at others, among other issues.
This kind of compiler/runtime feedback about source code is really interesting and (imo) under-studied. Especially when you take into account something like PGO data.
This is not always possible. Consider the monomorphized output of a generic function. An operation may be dead in one instance but not generally
That kind of feedback is also possible within this framework in theory. It depends on at what level the abstract interpreter is operating. If it’s the source level then it’s easy, but propagating that from an IR to source code is, shall we say, an open question.