1. Lean как движок для DSL’ов
Lean (особенно версия 4) — это язык общего назначения со встроенным механизмом макросов и метапрограммирования, позволяющим определять собственный синтаксис и управлять компиляцией. То есть вы можете:
Объявлять свои синтаксические конструкции, близкие к «человеческому» языку домена (например, языка описания банковских документов).
Автоматизировать (через метапрограммирование) генерацию определений и доказательств или упрощать их написание.
Таким образом, в принципе можно построить DSL, в котором финансовый аналитик работает не напрямую с функциональным/логическим Lean, а с «читаемым» языком, который «под капотом» порождает Lean-формулы, Lean-объекты и т. д.
Примерно так же в Coq или Agda иногда делают DSL’ы для описания протоколов, логических схем или теоретико-категорных конструкций. В Lean 4 это даже немного проще, потому что там есть развитая система макросов и возможность использовать более «привычный» синтаксис.
Проблема тут в том, что чем более «гуманитарным» вы делаете DSL, тем сложнее/длиннее будет «мост» между формулами в DSL и внутренним «ядром» Lean, и тем больше придётся вкладывать в поддержку метапрограммирования и генерации доказательств. Но зато конечным пользователям (например, аналитикам) можно действительно дать более привычный язык описания моделей и свойств.
2. DSL для заявлений (теорем) против DSL для доказательств
Важный момент:
DSL для описания предметной области (например, «вот у нас есть платежи, у них есть поля from, to, amount…», «вот ограничения по лимиту…») — это одно. Здесь мы хотим, чтобы пользователи писали модели и правила.
DSL для собственно доказательств (то есть для скриптов-тактик, которые шаг за шагом выводят формулу из посылок) — это совсем другое.
Как правило, от прикладных специалистов (например, финансистов) мы хотим, чтобы они формулировали теоремы и ограничения на уровне «Если Payment валиден, то после обработки сумма на счёте уменьшится ровно на Payment.amount», etc. Но не ждали от них, что они будут вручную «гидить» Lean-тактики, расписывая все промежуточные леммы.
Как это можно упростить
Автоматическая/полуавтоматическая доказательная среда.
Можно встроить в Lean (через метапрограммирование) вызовы SMT-решателей, автоматических теорем-доказчиков, построителей ProofTerm и т. д. Тогда пользователь формулирует theorem MyStatement : Prop := ..., а система пытается автоматически вывести доказательство. Если доказывается, – отлично, если нет, – просит доработать.
- В Lean есть встроенный
simp, linarith, tauto, а также возможность вызывать внешние инструменты вроде Z3.
Готовые шаблоны доказательств для типовых случаев.
Если бизнес-логика повторяется («Проверка баланса», «Проверка реквизитов», «Сумма неотрицательна»), то эти леммы можно заранее «зашить» в библиотеку, и пользователь просто пишет by auto_banking_tactics — что-нибудь в таком духе.
Фреймворк «декларативного» объявления свойств.
К примеру, пользователь только говорит «Payment.amount <= balance(fromAcc)» на «бизнес-языке DSL». А за кулисами это превращается в Lean-формулу (p.amount <= p.from.balance). Система либо доказывает сразу, либо выдаёт контрпример или рекомендации.
Таким образом, да, можно сделать «DSL для теорем» более высокого уровня, чтобы свести к минимуму ручное написание тактик. Но это, конечно, серьёзная проектная работа: вам нужно продумать, какие типовые шаги доказательства встречаются, и как их «зашить» в автотактики.
3. Multi-level modelling и прочие проблемы MOF
MOF (Meta-Object Facility) имеет ограничения, в том числе когда мы пытаемся делать многоуровневые модели (например, когда объект в одной модели становится метаклассом для другой модели и т. д.). В Lean у вас нет формальных препятствий для подобных «многоуровневых» конструкций, кроме того, что надо аккуратно следить за универсами (universe levels) и не попадать в парадоксы вроде Girard’s paradox. Но Lean из коробки умеет работать с иерархиями типов (Type u, Type v) и т.д., так что многоуровневые модели можно задавать довольно естественно.
Более гибкая система, чем MOF
В самом деле, Lean — это в первую очередь типизированная теория, и вы можете свободно выражать там иерархии понятий, плюс доказывать факты про них. MOF в UML-мире исторически был заточен под относительно простой 4-слойный «пирамида-сэндвич» подход (M0 – M1 – M2 – M3). Если у вас сценарии, где нужны более гибкие «мульти-левел» концепты, Lean (или Coq, Isabelle) в этом отношении гибче.
4. Насколько реально снизить порог входа
Порог входа в Lean сам по себе высок для новичков, особенно для «не-технических» пользователей. Но:
Слой DSL действительно может от этого барьера скрыть 80–90% сложности, если он хорошо спроектирован. Пользователь видит «свою» предметную лексику, пишет что-то, похожее на псевдо-код, — а Lean-макросы подставляют правильные определения и вызывают нужные тактики.
При возникновении сложных неавтоматизируемых доказательств, всё равно придётся либо подключать эксперта (который умеет «ручками» дотащить доказательство), либо как-то упрощать/изменять модель.
Но общий опыт показывает, что возможно построить удобный DSL (как в TLA+ или Alloy, где пользователи пишут декларативные спецификации, а автоматический движок их проверяет). Lean просто более универсален, но требует больше ручного труда, чтобы сделать такой «гладкий» DSL.
5. Практическая реализация: «да, но…»
Да, это всё реально и уже есть немало проектов, где создаются узкоспециализированные DSL, упрощающие жизнь не-экспертам в формальных методах.
Но каждая такая система — практически «мини-исследовательский проект». Нужно:
Спроектировать DSL (синтаксис, семантику, правила).
Написать метапрограммы, макросы Lean, автотактики и т.д.
Создать библиотеку готовых лемм для типовых паттернов.
Сформировать «туториалы», «best practices» и инструменты, чтобы пользователь мог работать без погружения во внутренности Lean.
Это достаточно большой пласт работ, но результат может быть очень мощным: пользователи получают DSL с «волшебной» возможностью генерировать код, проверять корректность моделей, и даже генерировать/проверять формальные доказательства «под капотом».
Итог
Сформулировать на уровне DSL (а не голого Lean) и метапрограммирования — вполне реально, если вы готовы вложиться в разработку такого фреймворка.
Автоматизация доказательств тоже достижима, хотя и 100% «автопилота» не всегда бывает, в сложных случаях нужна помощь эксперта по Lean.
Multi-level modelling и другие «сложные» аспекты MDD можно выразить гораздо гибче, чем в MOF.
Порог входа можно ощутимо снизить DSL’ом и автотактиками, но надо понимать, что в случае нештатных ситуаций всё равно потребуется «ручное» proof engineering.
В целом подход «DSL + Lean» даёт очень большой спектр возможностей: от простой структурной проверки до формальных теорем, от генерации кода до интерактивной проверки корректности. Поэтому да, это действительно может быть тем «здоровым балансом» между теоретической формальностью и практическим удобством, если грамотно всё организовать.
