* http://www.lsv.fr/Publis/PAPERS/PDF/Sch-aiml02.pdf
* http://www.lsv.fr/Publis/PAPERS/PDF/DLS-jcss-param.pdf
* https://www.cis.upenn.edu/~alur/Zohar03.pdf
What's important to put those results in context for those who are not familiar with the subject is that, in the context of complexity theory, the "model checking problem" does not refer to the complexity of a particular model checker algorithm, but to the inherent complexity of the problem of deciding whether a program M satisfies some property 𝜑 (i.e. whether M is a model of 𝜑 in the formal logic sense). The "model checking problem" is the closest to a mathematical description of what we usually mean when we talk of "reasoning about a program."
I've summarized these results and more here: https://pron.github.io/posts/correctness-and-complexity
>Here, too, there are theoretical results showing that increased expressiveness cannot lead to cheaper reasoning, which is not an obvious result even in the worst case (because there are far fewer "compressible" programs than non compressible ones).
I find that very interesting. Do you have a source for it?