A minimal (<500 LOC) programming language capable of proving theorems about its own terms.
There are big and small programming languages out there. C++ and Haskell are big languages. Other languages, such as Brainfuck, are so simple they could be implemented in 317 Python characters. The Lambda Calculus is popular for being a simple language that serves as the foundation of many functional programming languages.
Despite being turing-complete, there is one thing those languages can't do: expressing and proving mathematical theorems about its own terms. The few languages that can do that are rather big: Idris, Agda, Coq and Isabelle are examples. Some languages like the Calculus of Constructors (such as implemented on Haskell-Morte-Library) are small and capable of expressing and proving mathematical theorems about its own terms, but, since their expressivity is very limited, they're not useful for proving useful properties about everyday programs and applications. Until recently, we had no language that was both small and featured practical theorem proving.
Cedille is a language developed by Aaron Stump, aiming to solve that problem, among others. It is capable of proving useful theorems about its own terms, yet can be implemented in a very small amount of code. Cedille-Core is an attempt at implementing its core as tersely as possible.
The rules are implemented as described on this paper. Here is a preview:
This is just an initial attempt. It is fully untested, probably bug-ridden, certainly contains a lot of typos, etc. In fact, I'm still in the process of understanding Aaron's work, so chances are it has even deeper misunderstandings that could require major rewrites. This currently serves mostly as an initial step to better understand his work.