What makes a language (and its type-system) capable of proving theorems about its own terms? I've recently attempted to implement Aaron's Cedille-Core, a minimalist programming language capable of proving mathematical theorems about its own terms. I've also proven induction for λ-encoded datatypes on it, which made clearer why his extensions would be necessary.

Nether less, I'm still left wondering where those extensions came from. Why they are what they are? What justifies them? I know, for example, that some extensions, such as recursion, ruin the language as a system for proofs. If I decided to also extend CoC with other primitives, how would I justify? I understand a proof of normalization is necessary, but that doesn't prove those primitives "make sense".

In short, what specifically what qualifies a language (and its type-system) as a 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)