А нафига он нужен, умный такой, язык-то?

Есть большие сомнения даже в том, что ада-вская типизация как-то повышает надёжность, по сравнению с Обероновской.

Достаточно убрать смешение разных слоёв из фокуса внимания (т.е. позволить программисту забыть о машинном представлении, неявных приведениях типов и т.п.; а дать ему просто надёжное типизированное число; точно так же дать простой неломаемый указатель...) - и не будет этот программист делать глупых ошибок в выражениях и т.п. Потому что эти выражения - основная его работа, смысл программы. Раньше он отвлекался на всякую дрянь инструмента, не отвлекается - и отлично. А дальше усиливать контроль - особо сильного эффекта для качества ожидать не стоит. А вот как это повлияет на компилятор и рантайм - неясно. Поробуйте для разминки хотя бы ответить на вопрос, как эти механизмы будут себя вести при разнесении связанных соотношениями типов по разным модулям, в условиях раздельной компиляции, а тем более динамической загрузки?

Языков с усиленным статическим контролем много, только, как правило, такой контроль требует глобального анализа. И ставит крест на раздельной компиляции (тот же контрактно-ориентированный Эйффель вот, насколько я помню, её не поддерживает).

Баланс - штука тонкая.