[Pitch] Dependent Types & Universes (Stage 1 of Proof-Driven Development?)

Just as a reference: I mentioned this topic in the topic Dreaming of a “harmless” language mode just created by me.