Провёл собственное исследование по языкам программирования будущего.

В целом, дядька Боб правильно уловил ветер и выдвинул правильные требования к языку программирования для AI:
- гомоиконичность;
- явные типы;
- никаких скрытых потоков управления;
- контракты встроены в язык.

Но это пока просто идея. Не реализовано даже формальной верификации контрактов. Типы явные, но это скорее аннотации, чем Хиндли-Милнер. Нет алгебраических типов с exhaustive matching (хотя tagged unions упомянуты). Нет вывода типов.

Если цель - ИИ как полноценный разработчик, нужен язык, который максимизирует вероятность того, что сгенерированный им код корректен. Это значит: сильная система типов (компилятор ловит ошибки ИИ), простота (меньше галлюцинаций), достаточный объём кода в обучающих данных, и путь к формальной верификации.

Lean 4 - стратегически самый интересный, но практически самый рискованный. Если через 5-7 лет Lean станет практическим языком программирования, выбравшие его сейчас окажутся впереди всех. Но не сегодня.

На сегодняшний день выделяются два языка.

Rust - первый кандидат. Огромный объём обучающих данных, ИИ пишет на нём уверенно. Borrow checker отсекает ошибки с памятью. Система типов ловит логические ошибки. Verus, rocq-of-rust, Aeneas для верификации. Экосистема зрелая. Один минус - сложность языка увеличивает вероятность, что ИИ сгенерирует компилируемый, но неидиоматичный код. Тем не менее, строгость компилятора это компенсирует.

Ownership-модель - это фундамент, на котором можно строить доказательства.

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

OCaml - второй кандидат. Меньше обучающих данных, но язык проще, и паттерны более предсказуемые. Алгебраические типы и exhaustive pattern matching - идеальный формат для ИИ-генерации: он описывает все случаи, компилятор проверяет, что ИИ ничего не пропустил. Gospel (Generic OCaml SPEcification Language) - tool-agnostic язык формальных спецификаций для OCaml.

Именно поэтому OCaml используется в финтехе. Экосистема, правда, уступает Rust.

Вишенка на торте - Camlp5. Это OCaml с Lisp-синтаксисом. Типы, компиляция, всё как в OCaml, но добавлена гомоиконичность. S-выражение - это одновременно и программа, и структура данных, которую можно анализировать, трансформировать, генерировать другой программой. Это не макросы как синтаксический сахар - это фундаментальное свойство: программа может порождать программы так же естественно, как оперировать числами.

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

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

Это возвращает нас к тому, с чего начался ML (Робина Милнера) - к языку, созданному для доказательства теорем. Круг замыкается.

Милнер в начале 1970-х в Эдинбурге строил LCF - Logic for Computable Functions - систему для доказательства теорем. Ему нужен был язык, в котором на уровне системы типов невозможно было бы сконструировать невалидное доказательство. Так появился ML - Meta Language.

Пятьдесят лет спустя мы приходим к той же задаче, только с другой стороны. Милнер хотел, чтобы человек писал доказательства, а машина их проверяла. Мы идём к тому, что машина будет писать код, а формальная система - проверять его корректность. Задача та же - гарантия корректности через типы. Только роли поменялись.

ML был создан как язык для мира, где код должен быть доказуемо правильным. Этот мир тогда не наступил, потому что индустрии было важнее "быстро и дёшево", чем "правильно". Но если генерация кода становится бесплатной, а цена ошибки растёт - "правильно" побеждает. И оказывается, что фундамент для этого был заложен полвека назад в Эдинбурге.