Здесь просто мысли… даже, скорее, гипотеза, которая давно жила во мне, и в связи со статьёй Типы и тесты нашла, наконец, какой-то выход. Это не первый раз, когда я сталкиваюсь со спором между (условно) "типизаторами" и "тестировщиками", в одном или двух даже участвовал.
И у меня возникла ощущение, что для "типизаторов" центральное место в разработке занимает проблема правильности. Программа, которая "работает правильно" только в некоторых случаях, судя по всему, для них похожа на стоящие часы — да, они пару раз в сутки показывают правильное время, но на самом деле они же не работают!
Отсюда логично выплывает идея разработки как сборки системы из уже доказанно-правильных кусков. Если их ещё и собрать правильно, то и вся программа будет правильной. Такими "кусками" являются типы.
Данная трактовка, возможно, является ошибочной — знатоки Type-Driven Development меня поправят.
Вероятно, именно из этих предпосылок вытекает восприятие TDD как как тестирования — попытку обосновать правильность программы. И, разумеется, с их точки зрения TDD выглядит странной и очевидно бессмысленной идеей: доказывать правильность в общем случае, перебирая частные случаи, глупо — сил и времени потратишь много, а результат для бесконечных или очень больших множеств входных значений будет ничтожным.
Но на самом деле суть Test-Driven Development к тестированию имеет очень мало отношения. TDD следует воспринимать как воплощение стратегии "разделяй и властвуй": давайте сначала напишем программу, которая будет правильно вести себя всего в одном случае; потом добавим ещё один и попробуем обобщить реализацию; если результат не удовлетворяет, добавляем ещё один и снова обобщаем… — до тех пор, пока мы не будем вполне уверены в том, что написали практически правильную программу.
Да, здесь ставится немного другая цель — не написать такую программу, которая всегда работает правильно, а такую, которая лишь на практике работает правильно.
Очевидно (для меня), что Test-Driven Development — это построение программной системы по индукции.
Можно ли тогда утверждать, что Type-Driven Development — это построение программной системы по дедукции?
