История изменений

нужно либо надеяться на то, что тесты покрывают изменённый кусок, либо сидеть и вручную всё проверять

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

Это не лунное откровение, для получения которого нужно слетать на ракете на Луну.

Тогда тебя не затруднит вместо пространных рассуждений в вакууме привести конкретные цифры, показывающие, что использование типизированного вместо динамически проверяемого, при прочих равных (компетенция, опыт с инструментом, область разработки), повышает твою продуктивность на M>0, не смотря на необходимость ублажать компилятор, а количество ошибок сокращает на N>0.

Пока что мои наблюдения показывают, что по факту профит не наблюдается. И, похоже, не я один такой глупенький:

Robert Martin:

I found that type issues simply never arose. My unit tests kept my code on the straight and narrow. I simply didn’t need the static type checking that I had depended upon for so many years [1].

Bruce Eckel:

To claim that the strong, static type checking constraints in C++, Java, or C# will prevent you from writing broken programs is clearly an illusion (you know this from personal experience). In fact, what we need is Strong testing, not strong typing [1].

ADT в OCaml сильно меняет расклад сил и твои, например, сортировки гарантированно сортируют? Не сортируют. В Idris’е для такого юзкейса неплохо было бы написать доказательство доказательства. Похожая ситуация в Spark (High Integrity Software [2003], Barnes, страница 375).

нужно либо надеяться на то, что тесты покрывают изменённый кусок, либо сидеть и вручную всё проверять

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

Это не лунное откровение, для получения которого нужно слетать на ракете на Луну.

Тогда тебя не затруднит вместо пространных рассуждений в вакууме привести конкретные цифры, показывающие, что использование типизированного вместо динамически проверяемого, при прочих равных (компетенция, опыт с инструментом, область разработки), повышает твою продуктивность на M>0, не смотря на необходимость ублажать компилятор, а количество ошибок сокращает на N>0.

Пока что мои наблюдения показывают, что по факту профит не наблюдается. И, похоже, не я один такой глупенький:

Robert Martin:

I found that type issues simply never arose. My unit tests kept my code on the straight and narrow. I simply didn’t need the static type checking that I had depended upon for so many years [1].

Bruce Eckel:

To claim that the strong, static type checking constraints in C++, Java, or C# will prevent you from writing broken programs is clearly an illusion (you know this from personal experience). In fact, what we need is Strong testing, not strong typing [1].

ADT сильно меняет расклад сил и твои, например, сортировки гарантированно сортируют? Не сортируют. В Idris’е для такого юзкейса неплохо было бы написать доказательство доказательства. Похожая ситуация в Spark (High Integrity Software [2003], Barnes, страница 375).