He appears to be right in saying "Type checking is actually a special case of abstract interpretation". The paper that presented Abstract Interpretation to the

He appears to be right in saying "Type checking is actually a special case of abstract interpretation". The paper that presented Abstract Interpretation to the world concludes: "It is our feeling that most program analysis techniques may be understood as abstract interpretations of programs. Let us point out ... type verification..." https://www.di.ens.fr/~cousot/publications.www/CousotCousot-POPL-77-ACM-p238--252-1977.pdf https://www.di.ens.fr/~cousot/publications.www/CousotCousot-... That said, abstract interpretation promises that the absence of reports proves the absence of the errors that the sound static analyzer implementing it is designed to catch. Provided that you do not abuse casts/unions, the absence of warnings/errors from a compiler's type checking on a strongly typed language should prove an absence of type errors, which does sound like what abstract interpretation promises. Lastly, I need make time to actually read that paper. I have only read a very small part of it.