Три проверяющих, у которых разные стандарты
В процессе создания программы ваш код оценивают три совершенно разных «судьи».
Первый — компилятор. Ему важно только одно: соблюдены ли правила языка? Он проверит синтаксис, поверхностно — типы данных, убедится, что все переменные объявлены. Но вопрос «решает ли код правильную задачу?» компилятор даже не рассматривает. Ему всё равно, что функция поделит число на ноль или выйдет за границы массива. Его типичная реакция на ошибку выглядит так: «Тип Int не соответствует типу String».
Второй проверяющий — заказчик или тестировщик. Этому уже не всё равно. Он проверяет бизнес-логику, краевые случаи, соответствие требованиям. Его реакция на ошибку: «При вводе минус одного программа падает». И это уже проблема.
Третий — самая строгая инстанция. Это инструменты формальной верификации вроде Coq или Agda. Они требуют математического доказательства, что все возможные пути выполнения программы корректны. Они скажут: «Вы не доказали, что индекс всегда находится в границах массива». С ними работают единицы — обычно там, где цена ошибки невероятно высока.
Что делать, если код нравится компилятору, а заказчик находит ошибки?
Срочно идти учить академическую теорию типов — про кучу Карри-Говарда, гомотопии и аксиому унивалентности Воеводского.
Шутка.
Обычному разработчику нужна не теория типов, а практика проектирования, управляемого типами (type-driven design). Разница в твою пользу.
Академическая теория типов отвечает на вопрос «почему это работает?». А type-driven design отвечает на вопрос «как сделать так, чтобы неправильные программы не компилировались?». И второму может и должен научиться любой разработчик уровня мидл.
Три простых приёма без погружения в теорию
Первый приём: сделайте ошибки невозможными на уровне типов.
Вместо того чтобы писать функцию деления, которая принимает любые числа, создайте отдельный тип «не ноль». В TypeScript это можно сделать через так называемые бренды (специальные метки типов). Тогда функция деления будет принимать только числа, которые гарантированно не равны нулю. Если попытаться передать ноль — код просто не скомпилируется. Заказчик физически не сможет получить деление на ноль, потому что такого кода не существует.
Второй приём: используйте типы для бизнес-логики.
Частая ошибка — путать идентификаторы разных сущностей. Разработчик случайно передаёт идентификатор заказа туда, где ожидается идентификатор пользователя. В обычном коде обе переменные имеют тип «строка», и компилятор молчит. Решение — создать два разных типа: UserId и OrderId. Да, внутри это те же строки. Но для компилятора они разные. Перепутать их теперь невозможно.
Третий приём: показывайте заказчику корректность.
Не каждому заказчику нужны формальные математические доказательства. Ему нужна "работающая" программа. Лучшее доказательство для заказчика — это отсутствие ошибок на проде.
Путь к надёжному коду — четыре уровня сложности
Первый уровень — самый простой. Хорошее покрытие юнит-тестами и интеграционными тестами. Этого достаточно для большинства проектов.
Второй уровень — property-based testing. Вы не пишете отдельные тесты для каждого значения. Вы описываете свойства, которым должна удовлетворять функция, и инструмент (вроде QuickCheck для Haskell или fast-check для JavaScript) сам генерирует сотни случайных входов и проверяет свойства. Ошибки, которые заказчик находил в краевых случаях, такой подход ловит автоматически.
Третий уровень — контрактное программирование. Вы явно описываете предусловия и постусловия функций. В языках вроде TypeScript это делается через бренды, о которых мы говорили. В более строгих языках — через встроенные контракты.
Четвёртый уровень — зависимые типы. Это уже территория языков вроде Idris, Lean или F-star. Здесь вы можете написать тип функции, который гарантирует, что индекс никогда не выйдет за границы массива, потому что это записано прямо в типе. Но это нужно только для критических систем: авионика, медицинское ПО, смарт-контракты на большие суммы.
Кому действительно нужно учить академическую теорию типов?
Парадокс в том, что обычному кодеру — почти никогда.
Вот реальные сценарии, когда без неё не обойтись:
- Вы пишете системы, где ошибка стоит человеческих жизней или миллиардов долларов.
- Ваш заказчик требует математически строгих гарантий, которые невозможно получить тестами.
- Вы создаёте библиотеку, которую будут использовать тысячи разработчиков, и хотите сделать API абсолютно безопасным.
В остальных 95 процентах коммерческой разработки достаточно хорошей системы типов (как в TypeScript, Rust, Swift, Scala или даже Haskell без зависимых типов) плюс культуры их использования.
Что делать прямо сейчас, если заказчик находит ошибки?
Первое. Начните писать property-based тесты на краевые случаи. Они часто находят те же ошибки, что и заказчик, но до того, как код попадёт в прод.
Второе. Внедрите в команде практику «типы, которые не лгут». Используйте специальные обёртки вместо null. Создайте тип NonEmptyArray вместо обычного массива там, где пустой массив — это ошибка. Компилятор сам заставит вас обрабатывать проблемные случаи.
Третье. Если этого недостаточно — посмотрите в сторону Idris или Lean. У них есть отличные туториалы для программистов, которые не требуют предварительного погружения в теорию категорий.
Итог
Выражайте требования в типах, пишите property-based тесты, делайте неправильные состояния непредставимыми.