Язык программирования Lean давно заслужил репутацию одного из самых мощных инструментов для формальных доказательств и интерактивного программирования. Совмещая функции системы доказательств с современными функциями разработки, Lean предлагает уникальный опыт, который понравится как математикам, так и программистам. Однако визуальные и практические примеры применения языка нередко вызывают вопросы: чем Lean может заинтересовать пользователей, помимо формальностей и академических задач? Вдохновляющий эксперимент с воспроизведением анимации «Bad Apple!!» с использованием Lean тактик не только демонстрирует мощь этого языка, но и раскрывает тонкости работы с системой в реальном времени, взаимодействия с редактором и создания нетривиального кода для решения уникальных задач. «Bad Apple!!», культовый анимационный ролик, известен во всем интернете своей монохромной палитрой и сложностью воспроизведения в нестандартных средах. Нечто подобное заставляет задуматься о том, насколько глубоко можно интегрировать анимацию, игру с изображениями и взаимодействие с системой программирования.
Изначально идея показалась простой: воспроизвести видео в редакторе с помощью Lean. Однако на практике возникло множество ограничений и вызовов. Lean как язык и как система доказательств использует концепцию тактик — специальных метапрограмм, которые помогают упростить и автоматизировать доказательства. В отличие от обычных функций, тактики можно понимать как ходы в интеллектуальной игре, при которых изменяется состояние доказательства до тех пор, пока оно не приобретёт конечный вид истины. Однако возможности тактик намного шире.
Они могут взаимодействовать с файловой системой, выполнять внешние процессы и даже запускать Javascript-встраиваемые виджеты в редакторе VSCode, что открывает перспективы для создания интерактивных и мультимедийных инструментов. Первой попыткой было использование виджета, встроенного в infoview VSCode. Разработчик создал виджет на React, который воспроизводит видео «Bad Apple!!». Это можно считать «читерским» решением с точки зрения чистоты реализации на Lean, но оно ярко иллюстрирует возможности кастомизации среды. Видео запускается прямо в панели редактора, что позволяет познакомиться с необычным типом вывода информации.
Однако такое решение не раскрывает всех возможностей Lean тактик, и поэтому была предпринята попытка создать то же самое целиком на Lean, без использования внешних биллингов и плееров. Тут начинается глубокое погружение в метапрограммирование: тактики становятся не просто инструментом, а способом управления состоянием, отображения кадров анимации и даже симуляции видео в текстовом виде. Автор проекта использовал подход, при котором каждый кадр видео преобразовывался в отдельное изображение формата PPM — простого формата, который легко обрабатывать. Затем каждая точка кадра конвертировалась в соответствующий символ в консоли, используя символы разной плотности, которые заменяли оттенки серого, имитируя переходы и тени. Интересной идеей стала замена символов на цветные эмодзи, что, несмотря на название, помогло расширить цветовую палитру и добавить выразительности рисунку.
Одним из главных вызовов стала работа с большим числом кадров. В Lean, как и во многих строго функциональных языках, управление состоянием — дело сложное. Тактики выполняются последовательно, и редактор обновляет свое состояние только после завершения тактики. Следовательно, полная анимация в реальном времени невозможна в рамках одной тактики; это накладывало ограничения на частоту кадров и плавность воспроизведения. Для решения было придумано решение на уровне макросов: код автоматически генерировал серию вызовов тактики, каждая из которых выводила один кадр, а затем переходила к следующему.
Несмотря на техническую сложность, это позволило показать анимацию в редакторе, пусть и с ограничениями по скорости и ресурсоёмкости. Однако это привело к замедлению работы VSCode, так как он не предназначен для мгновенного отображения тысячи сообщений журнала с высокой частотой. Еще одна интересная инженерная деталь — использование файла с индексом текущего кадра, что позволяло отслеживать прогресс вывода и синхронизировать его с текущим временем. Таким образом, тактика читает индекс и время из файла, выводит очередной кадр, обновляет индекс и учитывает задержки для воспроизведения с приблизительно нужной частотой. Этот трюк позволяет добиться относительно плавной и синхронизированной анимации.
Примечательно, что Lean позволяет тактикам работать с внешними ресурсами — файловой системой, запуская shell-процессы и даже взаимодействуя с сетевыми API. В данном проекте это проявилось в использовании ffmpeg для преобразования оригинального видео в серию изображений PPM и запуске mpv для воспроизведения фонового звука. Этот подход иллюстрирует, насколько язык с доказательной семантикой оказывается мощным мета-языком, способным в себя интегрировать классическую развлекательную функциональность. Задумываясь о будущем Lean как языка, проект с «Bad Apple!!» показывает, что за счет уникальных возможностей Lean возможно создавать сложные интерактивные системы, которые выходят далеко за рамки математики или статических доказательств. Свобода метапрограммирования, хорошая интеграция с современными средами разработки и мощные средства взаимодействия с окружающим миром делают Lean необычайно перспективным для творческого применения.
Стоит особо отметить, что исполнительный код тактик — это не обычный функциональный код без побочных эффектов. Тактики могут выполнять любые операции с окружением и задавать практически любые значения состояния. Такая свобода приводит к необходимости аккуратно подходить к написанию и поддержке метакода, чтобы не столкнуться с непредсказуемыми последствиями. Впрочем, это также открывает двери для самых разнообразных экспериментов, которые в других языках оказались бы невозможны или чрезмерно сложны. Несмотря на технические сложности и необходимость жертвовать производительностью при визуализации десятков кадров в секунду, данное исследование Lean и возможностей тактик вдохновляет к дальнейшему развитию и применению языка.
Современное развитие языков и доказательных систем часто направлено на расширение границ применимости — и интеграция с мультимедиа, аудио и визуальными эффектами может стать одной из интересных частей этого пути. В заключение, проект воспроизведения «Bad Apple!!» с помощью Lean тактик — это одновременно и забавная демонстрация, и глубокое техническое исследование языка Lean, которое показывает, как традиционно академический инструмент можно перекроить для решения современных и крутых задач. И хотя качественная анимация в таком формате пока остаётся большим вызовом, прорывы в доступности инструментов и возможностях метапрограммирования делают будущее Lean очень многообещающим.
