На подходе обзор Lean 4
Приветствую!
Я нашёл язык, в котором можно писать без багов! Ну, почти...
Это Lean 4. В нём можно записать любое желаемое свойство программы в типах функций, и потом проверить.
Звучит заманчиво. Но за чей счёт банкет? Такое раздолье не бывает бесплатно, скажете вы. И будете правы...
Lean основан на зависимых типах. Когда мы задаём типы функции мы создаём теорему. Когда мы её реализуем, и компилятор принимает реализацию, теорема доказана.
Например, есть у нас функция gcd(a, b: Nat), которая реализует алгоритм Евклида и находит наибольший общий делитель натуральных чисел a и b. Мы можем записать теорему, что от перемены их мест результат не меняется:
```
theorem gcd_comm {a b : Nat} : gcd a b = gcd b a := by
```
Это вроде просто. Но ведь это теорема. А теоремы нужно доказывать!
В данном конкретном случае доказательство занимает восемь строк. Это не сложное доказательство. Ведь сама функция gcd занимает всего четыре строчки (плюс четыре строчки на доказательство того, что она всегда завершается).
Но доказательство более сложных функций даётся сложнее. Секрет состоит в том, чтобы сложных функций у нас было как можно меньше! Тогда доказать свойства простых функций часто бывает тривиальной задачей! Иногда Lean может доказать их автоматически!
Каждую большую функцию нужно обязательно разбивать на несколько мелких! Их свойства мы доказываем относительно легко и просто. После этого строим сложную, и исходя из уже доказанных свойств наших кирпичиков, так же без колоссальных усилий доказываем свойства наших построек.
На бумаге звучит не плохо. Разбиение сложного на простые части действительно позволяет упростить разработку с доказательством. Но даже так доказательство корректности сложной программы - это достаточно сложно.
Но что замечательно, мы вообще не обязаны доказывать всё подряд! Lean - это просто хороший функциональный язык программирования. Говорят, достаточно быстрый! Мы можем писать на нём примерно как на Haskell, а доказательства использовать только там, где это действительно оправдано, и где цена ошибки высока.
Как функциональный язык программирования, Lean отсекает огромное количество багов просто за счёт того, что данные у вас неизменяемые. Плюс мощная система типов отсекает другую прорву багов. А для самых важный частей программы таки можно применить и всю мощь доказательств!
Я уверен, что Lean - это очень хороший и перспективный язык! Он позволяет нам быть уверенными, что наши программы работают так, как надо. А это очень важно. Кто любит баги? Наверное, только майнкрафтеры, которые их используют порой очень нестандартно. А в обычных программах баги не нужны!
Соглашусь, формальная верификация программ - это достаточно высокая цена за надёжность. Но она окупается, если код используется часто, как популярная библиотека, или если цена ошибки высока.
Сейчас гремит популярность ИИ в разработке. А ведь в его коде куча багов! Говорят, код он пишет довольно посредственный. Но если мы пишем доказательство, мы можем пожертвовать красотой кода в угоду скорости разработки Если доказательство корректно, оно корректно с вероятностью 99.99%! Главное самому задавать искусственному интеллекту цели для доказательства, а там уж он как-нибудь справится! Ладно, может и не справится, но генерация доказательств - это интересная исследовательская тема!
Ждите обзор Lean! Там я разберу все эти темы подробнее. Подписывайтесь, чтобы не пропустить этот обзор, и узнать о качествах этого замечательного языка.
