Что действительно делает программу великой? Скорость работы, поражающая воображение? Лаконичность и изящество кода, восхищающие коллег? Или, быть может, Архитектура, обещающая вечную гибкость? Тысячи лет все эти империи рушились перед лицом коварной Ошибки. Пришло время провозгласить манифест иной истины: высшая ценность программы — её Достоверность, и цель разработки — доказать, что программа безупречно воплощает замысел своего создателя. В данной статье мы рассмотрим инструменты и методы, которые превращают намерение программиста в неопровержимую теорему. Через формальную верификацию тривиального, но коварного ФиззБазза средствами Idris 2 мы покажем, как строить программы, чья правильность не вера, но математический факт. Зависимые типы — наш меч. Добро пожаловать в мир, где код не просто работает — он доказан. Рассуждать и доказывать