The theory and practice of static analysis differ greatly. In static-analysis research, the focus is commonly on analyses that are proven sound, apply to small calculi or toy languages, and use sophisticated techniques to achieve precision. In industry, static analyses are unsound, apply to real languages, and use simple techniques in order to scale to large programs.

Static-analysis researchers avoid unsound analyses, because it is not clear what one can formally say about an unsound analysis. Sure, it helps people in practice, but what precise statement can one make about it? Is the merit of an unsound analysis based purely on opinion?

I believe it is beneficial to characterize unsound analyses mathematically; to develop rigorous ways of evaluating them and formal models describing their behavior. Then, theoreticians would be able to approach unsound analyses systematically, and develop novel ways of reasoning about such analyses. In addition, practitioners would be able to compare the pros and cons of various analyses in a precise way.