> Type checking is actually a special case of abstract interpretation.

I'm not sure about that.

Maybe in regard to type level functions? But else? I'm skeptical.

Could you explain what you exactly mean? Preferably with some examples as I'm having a hard time to imagine something in that direction.

> For all we know, it may even be that dependent types can already express many complex uses of it;

That for sure! Otherwise, corresponding type systems wouldn't be considered being an alternative.

Depended types can express anything computable. (Which also makes them undecidable in general).

In theory, you can prove any property of a program using depended types. That's why they're the preferred method by now. But you can't bold on such thing after the fact usually. Your language needs to be pure to benefit form the proving powers of depended types. So no hope for C and such like.

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

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.

You could model C in a dependently-typed language by embedding the C abstract machine and C program expressions in it. Then you could use the Poincaré principle applied to C-program fragments to perform any "abstract interpretation" of them and derive any property you might care about. So it looks like the Poincaré's principle (as it was named by Barendegt) is the actual "missing link" that would enable you to generalize from purely syntax-based analysis (as in the traditional definition of type systems/type checks) to "interpretation" of a more general sort.

> Type checking is actually a special case of abstract interpretation. For all we know, it may even be that dependent types can already express many complex uses of it; I don't think there's any literature that expressly tries to figure out how the two relate, beyond noting that abstract interpretation subsumes simple type checking.

See the paper that presented abstract interpretation to the world:

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