Dependent types

"Dependent types are useful not only because they help you express correctness properties in types. Dependent types also often let you write certified programs without writing anything that looks like a proof. Even with subset types, which for many contexts can be used to express any relevant property with enough acrobatics, the human driving the proof assistant usually has to build some proofs explicitly. Writing formal proofs is hard, so we want to avoid it as far as possible. Dependent types are invaluable for this purpose."



See Also