Есть такое важное понятие, как типо-безопасность, в computer science более известное как soundness. И есть также понятие логической консистентности, которое с ним часто путают. Так вот, soundness -- это про то, что термы "не могу ошибаться". Терм у нас может быть либо значением, либо его можно продолжать редуцировать дальше.

Например, мы определили деление как операцию только для ненулевых знаменателей. Тогда терм 'x / 0' нельзя далее редуцировать, но он при этом и не значение.

=
А логическая консистентность подразумевает, что не существует способа сконструировать терм из любого типа.

Ну например в F# возможно такое:

let rec foo() = foo()

Задайте foo любой тип, и получите терм этого типа.

Это означает, что данный язык плохо подходит для организации логических построений. А в общем случае все Тьюринг-полные языки логически неконсистентны.

=

И что из этого? Ну, не понимая такие вещи, вы не сможете продуктивно программировать на языках с зависимыми типами, да и вообще работать с HoTT-типами, следовать type-level программированию и метапрограммированию с dsl-ями, да и просто правильно применять генерики. И никогда не станете x1000 программистом.

Хватит уже лежать физиономией в салатах, поднимайтесь! :)