Reading your other comment, I'll concede that it's not impossible to encode these things into the type system. I don't think it will scale beyond toy examples (

Reading your other comment, I'll concede that it's not impossible to encode these things into the type system. I don't think it will scale beyond toy examples (at least until AGI is a thing). There are plenty of function names that represent highly specific business processes (and jargon) and I don't see how any type system will have enough context for that. Less bugs does sound good, but after a minute thought there still seem to be uncountably infinite bugs even in the presence of dependent types. Just a few less than without. :)