Подразделение Microsoft Research недавно опубликовало предварительный релиз Lean 4. Предыдущие версии Lean были сосредоточены на том, чтобы быть помощником по доказательствам — программным инструментом, который облегчает разработку строгих математических доказательств с помощью интерактивной совместной работы человека и машины. До сих пор язык Lean в основном применялся для оцифровки теоретической математики.

Главная цель Lean 4 — сделать Lean хорошим языком программирования, а не просто помощником по доказательствам. Синтаксис был переработан во многих отношениях, чтобы облегчить написание более широкого спектра программ. Был написан оптимизирующий компилятор, генерирующий эффективный код на языке C. Он обладает новой высокопроизводительной технологией управления памятью, помогающей избежать проблемных пауз во время работы, которые часто сопровождают такие инструменты (например сбор мусора), и при необходимости легко интегрируется с существующим кодом C/C++. В настоящее время Lean — в значительной степени самодостаточный язык, который написан на самом языке Lean.

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

Наша цель состояла в том, чтобы создать работающий контроллер на языке Lean. Это отличается от того, о чем обычно думают при использовании программ для доказательства теорем. Как правило, можно указать формальную модель контроллера, которая может опустить низкоуровневые детали, определить отражающие предположения аксиомы, которые, как ожидается, будут верны для окружающей среды, а затем попытаться доказать, что контроллер стабилизировал систему в мире, удовлетворяющем аксиомам окружающей среды. Это достойная цель, и мы хотели бы в итоге её достичь. Однако, поскольку при фактической реализации контроллера для этого проекта будет использоваться язык Lean, нам необходимо было включить детали низкого уровня, которые в противном случае могут быть опущены.

Мы начали с покупки двухколёсного робота за 90 долларов и стали проводить эксперименты с языком Lean. Мы проверили сгенерированный код на языке C и библиотеку времени выполнения и обнаружили, что код вполне переносим. К сожалению, предварительный выпуск библиотеки времени выполнения Lean содержит зависимости (например от библиотеки libgmp), и она слишком велика для контроллера робота на базе Arduino. К счастью, сгенерированный код легко запускается на компьютере Rasberry Pi. 

Мы приобрели 8-гигабайтную версию, чтобы скомпилировать Lean непосредственно в ней. Это добавило 80 долларов к стоимости нашего проекта, и мы вписались в наши необходимые аппаратные ограничения, а авторы Lean заинтересованы в решении проблем с размером библиотек времени выполнения.

Следующим шагом стало разделение существующего кода роботизированного контроллера для работы через последовательное соединение Bluetooth, чтобы запустить все алгоритмы управления на Rasberry Pi, сохранив при этом минимальный код для управления двигателем и считывания данных акселерометра на плате Arduino. Это было довольно просто, но потребовало использования сервиса Google Translate, чтобы понять комментарии в исходном коде. Исходный код после перевода комментариев можно посмотреть здесь, а разделённый на секции код Arduino после извлечения алгоритмов управления — здесь.

Затем мы транслировали код управления с языка C на язык Lean с помощью ручного, но довольно простого процесса. Версия Lean 4 в конечном счёте создаёт функциональные определения и обладает точностью, модульностью и композиционными преимуществами функционального программирования. Однако она имеет многофункциональный исходный язык, который позволяет использовать циклы for, мутабельные локальные переменные и структурированные операторы управления потоком, такие как break и continue. Внутри Lean 4 использует сложный процесс анализа для автоматической и прозрачной реструктуризации кода в функциональное определение. Это снизило уровень усилий, необходимых для портирования с языка C на язык Lean.

Написанный нами код Lean доступен широкой публике на Github. Основная функция пошагового управления BalanceCar.update выполняется каждые 5 мс. Для оценки ориентации робота по показаниям гироскопа и акселерометра (6 DoF IMU) используется фильтр Калмана. Контроллер PD принимает состояние ориентации в качестве входных данных и определяет скорость двигателя, таким образом замыкая контур управления.

После завершения портирования мы написали некоторый код на языке C, чтобы подключить код управления на языке Lean к последовательным API-интерфейсам Bluetooth, и опробовали его. Первоначальные результаты были занимательными, но не совсем правильными:

Это немного разочаровало, но такое случается в реальном программировании. Мы провели несколько тестов, внесли некоторые изменения, чтобы уменьшить задержку Bluetooth, и исправили в Lean-коде попутно обнаруженную ошибку. В итоге мы успешно создали работающего робота:

Как отмечалось ранее, это был всего лишь небольшой эксперимент для тестирования языка Lean в контроллере реального времени и работы, необходимой для ручного переноса кода с языка C на язык Lean. Мы ещё не проверили правильность контроллера (пока), но, когда у нас будет немного больше времени, мы планируем поработать над этим и интегрировать контроллеры на языке Lean в экосистему ROS, чтобы и другие люди могли опробовать его. У нас также есть более крупный проект, в котором языки Haskell и Lean, а также SMT-решатель используются совместно, чтобы создать проверенный декомпилятор от 64-разрядной версии с архитектурой x86 до LLVM. В будущем у нас будет больше информации об этом.

Вся работа, которую мы проделали для этого проекта, находится в открытом доступе, чтобы её могли попробовать выполнить те, кто в этом заинтересован. Мы намеренно использовали относительно недорогого робота, чтобы люди могли легко опробовать код. Так можно опробовать Lean лично или показать студентам, что вы можете писать реальные программы на этих языках. Если у вас есть какие-либо вопросы о проекте, вы можете пообщаться с нами на канале Lean Real-time Systems (Системы реального времени на языке Lean) сервиса Zulip.

Хочется поблагодарить авторов Lean, которые помогли сделать это возможным, а также Джоуи Доддса за комментарии, которые помогли улучшить эту публикацию.

Мы уже писали о том, как ML и компьютерное зрение используют на обогатительных фабриках, и если вы хотите научить роботов или машины видеть мир, принимать решения и действовать по ситуации, обратите внимание на наш курс "Machine Learning и Deep Learning" партнером которого является компания Nvidia.

Также можете взглянуть на профессию C++ разработчик, на котором можно прокачаться или освоить С++ с нуля. Приходите — будет сложно, но интересно!

Узнайте, как прокачаться и в других специальностях или освоить их с нуля:

• Профессия Data Scientist

• Профессия Data Analyst

• Курс по Data Engineering