Автор: Денис Буздалов · Heisenbug
Денис Буздалов работает в ИСП РАН с 2010 года: верификация авиационной электроники самолётов, тестирование криптопротоколов по формальным моделям, зависимые типы. Человек, который думает о корректности систем профессионально.
8 апреля 2022 года самолёт TAP Air Portugal в Копенгагене ушёл на второй круг в нестандартной ситуации — и левый двигатель не свернул реверс тяги. ПО было корректно сертифицировано. Баг проявился после 95 миллионов посадок и не воспроизводился ни в одной другой конфигурации. Самолёты так и продолжили летать с этим ПО спустя годы — исправление планировалось к 2025 году. Буздалов задаёт с этого вопрос: что вообще значит «хорошо протестировано», если такое возможно?
Его ответ: хорошее тестирование должно ставить систему в ситуации, о которых автор тестов даже не подумал. Property-based testing это умеет — описываешь свойства, а не примеры, фреймворк ищет опровержение на случайном входе. Но есть класс задач, где случайный вход почти всегда бессмысленен: сгенерировать программу, которая корректно тайпчекается, или граф с нетривиальными инвариантами наугад — значит получить 99% мусора. Буздалов показывает, как зависимые типы закрывают эту дыру: инвариант входных данных кодируется в типе, и генератор выводится автоматически через DepTyCheck.
Кому смотреть: всем, кто строит системы, где ошибки дорого стоят и плохо воспроизводятся вручную — не только авторам компиляторов, но и разработчикам протоколов, финансовых движков, встроенного ПО, любых систем с нетривиальными инвариантами на входе.
Из этого можно взять в работу: сформулировать для своей системы одно свойство вместо набора примеров и запустить на нём property-based тест. Не для сложных структур — просто как первый шаг к тому способу думать о тестировании, который Буздалов описывает.
