Годное расставление точек над i с ЛОРа. Поддерживаю. *1. примитивные системы типов (навроде как в хаскеле) могут отловить лишь примитивные ошибки, логика все равно тестируется. 2. тесты на логику падают на примитивных ошибках в том числе, то есть в итоге эти ошибки один хер не пропускаются и профит от системы типов в области гарантий становится де-факто сильно преувеличен. 3. Не примитивные системы типов чрезвычайно сложны в использовании, перспективы использования ЯП с подобными системами типов в качестве ЯП общего назначения - весьма смутны. Хотя, естественно, существует определенный класс задач, где этот инструмент весьма эффективен. 4. Из-за типодрочесртва CS последние десятилетия не развивается вообще никак - вместо поиска и развития альтернативных подходов легче написать диссер про никому не нужное расширение лямбда-хуямбда-омега-стрелки зигохистоморфическими препроморфизмами. Вообще, сложилось мнение, будто CS = исследования в области систем типов и больше исследовать нечего. Тупик, как есть. То есть, понятно, системы типов исследовать тупо _удобно_, но хотя бы в некоторой мере наука должна идти и от требований практики в том числе, потому что, блять, оно так всегда - полезные для практики задачи обычно неудобны. Хотя бы потому что помимо гарантии корректности у системы типов есть еще и конструктивистская функция. Но для адептов динамики это просто не понятно. Это для адептов статики непонятно, что есть и альтернативные ебле с типами подходы к разработке программ, потому что за узким статическим мирком для этих адептов жизни нет. И ты, кстати, ни о какой "конструктивистской функции" не упоминаешь - а прыгаешь по тредам, как еблан, и срешь везде на тему "но без типов даже факториала не напишешь".*