[acchow]

You're mostly describing why dependent types are useful (in preventing an entire class of errors).

The lambda cube is useful in comparing and reasoning about the features of type systems across languages.