What makes a language (and its type-system) capable of proving theorems about its own terms?
[Self-advertising follows, but I think that this is relevant.]

There are several possible approaches to this questions. One of the ways (that I explored during my PhD thesis in the context of an ML-like language) is to extend the type system with a first-order layer, so that terms of the language can be manipulated as objects of the underlying logic. Of course, you also need to include some predicates so that there is something to observe. In the case of my system, these predicates are term equivalences. In particular, if $t$ and $u$ are terms of the language, then the type $t \equiv u$ is only inhabited if $t$ and $u$ are indeed (observationally) equivalent. You can use first-order quantifiers to encode properties such as $\forall v, (\lambda x.x)\;v \equiv v$ in types, and they are proved by constructing programs inhabiting them.

Of course you can also assume equivalences, and there are several different forms of quantifiers (typed / untyped, universal / existential). This mechanism can be used to reason about any program (they do not have to be proved terminating or even typed). The only constraint is that programs that are used as proofs must be proved terminating by the system (arbitrary general recursion leads to inconsistency).

Here are a couple of references if you want to check this out:


https://lepigre.fr/files/docs/lepigre2017_pml2.pdf (recent paper with examples)
https://tel.archives-ouvertes.fr/tel-01590363 (PhD thesis in English)
https://github.com/rlepigre/pml (language implementation)