Зеленый тест врет: зависимые типы и мультиагентная система против QA-инструментов

Каждый день вы смотрите на зеленые галочки автотестов и верите им. Но инструменты, которые эти галочки рисуют, — валидаторы схем, движки JSONPath, API-фреймворки — сами написаны людьми и сами содержат баги, включая те самые heisenbug'и, что ловят вас в самый неподходящий момент.

В этом докладе я покажу машину, которая охотится за такими багами вместо человека. В ее основе — зависимые типы (Idris2/DepTyCheck): они позволяют генерировать входные данные, корректные по построению, — валидность здесь не проверяется постфактум, а гарантируется самим типом.

Дальше в дело вступает мультиагентная система: она прогоняет эти данные в поисках расхождения. Наведем этот прицел на широкий пул из вашего ежедневного стека — браузерная автоматизация, нагрузочное тестирование, API-фреймворки, валидаторы схем, движки JSONPath, парсеры протоколов — и посмотрим, где реализации одной и той же спецификации на удивление сильно расходятся между собой.

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

Вы уйдете с доклада, немного иначе глядя на свои зеленые галочки, — и с парой приемов, как заставить инструменты доказывать, что им можно доверять.