Microsoft Research recently published a pre-release of Lean 4. Prior versions of Lean focused on being a proof assistant – a software tool that facilitates the development of rigorous mathematical proof through a form of interactive human-machine teaming. The main application of Lean so far has been to digitize theoretical mathematics.
A major goal of Lean 4 is to make Lean a good programming language rather than just a proof assistant. The syntax has been reworked in many ways to make it easier to write a wider variety of programs. An optimizing compiler that generates efficient C code was written. It features a novel memory management technique that is highly performant and helps us avoid problematic runtime pauses that frequently accompany such tools (i.e., garbage collection), and it is easy to integrate with existing C/C++ code when necessary. Lean is now largely self-hosting and written in Lean itself.
To assess Lean’s suitability as a programming language for real systems, we set out to write a Lean implementation of a robotics controller running on a single board computer. To make things more interesting, we chose a controller for a two-wheeled robotics platform. If Lean programs are not able to provide real-time commands to the motors in response to sensor inputs, the system will literally fall down.
Our goal was to build a working controller in Lean. This is different from what one usually thinks of when using theorem provers. Typically, one would specify a formal model of the controller that may omit low-level details, define axioms that capture assumptions expected to be true of the environment, and then try to prove the controller stabilized the system in a world satisfying the environment’s axioms. This is a worthwhile goal and one we would like to pursue eventually. However, as the actual controller implementation for this project would use Lean, we needed to include low-level details that may be otherwise omitted.
We started by buying a $90 two-wheeled robot and began doing experiments in Lean. We inspected the generated C code and the runtime library and found that it was quite portable. Unfortunately, the pre-release version of the Lean runtime brings in dependencies (e.g., libgmp) and is too large for the Arduino-based controller on the robot. Fortunately, the generated code could run quite easily on the Rasberry Pi. We bought the 8GB version so we could compile Lean directly on it — this added $80 to our project’s cost. This fit within our desired hardware constraints and the authors of Lean are interested in addressing runtime library size issues.
The next step was to partition the existing robotic controller code to work over a Bluetooth serial connection to run all the control algorithms on a Rasberry Pi while keeping minimal code to control the motor and read the accelerometer data on the Arduino board. This was pretty straightforward but required some use of Google Translate to understand the code’s initial comments. You can see the original code after translating comments here and the partitioned Arduino code after extracting the control algorithms here.
Next, we translated the control code from C into Lean through a manual but fairly straightforward process. Lean 4 ultimately produces functional definitions and has precision, modularity, and compositional benefits of functional programming. However, it has a rich source language that permits use of for loops, mutable local variables, and structured control flow statements like `break` and `continue.` Internally, Lean 4 uses a sophisticated analysis process to automatically and transparently restructure the code into a functional definition. This reduced the level of effort required to port from C to Lean.
The Lean code we wrote is publicly available on Github. The primary control step function BalanceCar.update runs every 5ms. It uses a Kalman filter to estimate the robot orientation from gyroscope and accelerometer readings (6 DoF IMU). A PD controller accepts the orientation state as input and determines the motor speed thus, closing the control loop.
After finishing the porting, we wrote a bit of C code to connect the Lean control code to the Bluetooth serial APIs and tried it out. The initial results were entertaining but not quite right:
This was a bit disappointing but happens in real-world programming. We did some tests, made some changes to decrease Bluetooth latency, and fixed a bug in Lean we discovered along the way. In the end, we successfully created a working robot:
As noted earlier, this was just a small experiment to test Lean out in a real-time controller and the work required to manually lift C code into Lean. We haven’t verified the controller correctness (yet), but when we have a bit more time, we plan to work on this and integrate Lean-based controllers into the ROS ecosystem so more people can try it out. We also have a larger project using Haskell, Lean, and SMT solver together to produce a verified decompiler from 64-bit x86 to LLVM. We’ll have more information on that in the future.
All of the work we did for this project is publicly available to try out if you are interested. We intentionally used a relatively low-cost robot so that it is easy for people to try out the code. This could be a way to personally try out Lean or to show students that you can write real programs in these languages. If you have any questions about the project, you can chat with us on the Lean Real-time Systems Channel on Zulip.
We want to thank the authors of Lean for their help in making this possible, and Joey Dodds for comments that helped improve this blog post.