Вот, тащем-то, цитата-ответ на вопрос "зачем в ЯП вообще нужны типы":

Современные технологии разработки программного обеспечения располагают широким репертуаром формальных методов (formal methods),
которые помогают убедиться, что система ведет себя в соответствии с
некоторой спецификацией ее поведения, явной или неявной. На одном
конце спектра находятся мощные конструкции, такие как логика Хоара,
языки алгебраической спецификации, модальные логики и денотационные семантики. Они способны выразить самые широкие требования к
корректности программ, однако часто очень трудны в использовании и
требуют от программистов высочайшей квалификации. На другом конце спектра располагаются намного более скромные методы. Настолько
скромные, что автоматические алгоритмы проверки могут быть встроены в компиляторы, компоновщики или автоматические анализаторы
программ, а применять их могут даже программисты, не знакомые с теоретическими основами этих методов