*Bounty: 50*

*Bounty: 50*

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?