@dysfun I see the main promise of dependent types a bit less in compile-time proofs (although I realize that many see this as their main or even defining use case), but as something to effortlessly (!) express interesting properties in types. I even prefer if this then just creates run-time assertions instead of insisting on static checking from the beginning, and leaves it up to me to prove it later or not.