[benrbray]

Dependently-typed languages often work this way! See for instance "Inductively Defined Propositions" in Coq. (remembering, of course, that propositions are types [2], which proof assistants take quite literally)

[1] https://softwarefoundations.cis.upenn.edu/lf-current/IndProp... [2] https://homepages.inf.ed.ac.uk/wadler/papers/propositions-as...