Dependent types strictly just means being able to parametrize types with values. You can design many different types of PLs with this feature. You don’t need s

Dependent types strictly just means being able to parametrize types with values. You can design many different types of PLs with this feature. You don’t need strict reasoning for it to be useful like any other type level feature.