Robotics control in real time using the Lean language

Microsoft Research recently published a preview release Lean 4… Previous versions of Lean focused on being Evidence Assistant – a software tool that facilitates the development of rigorous mathematical proofs through the interactive collaboration of man and machine. Until now, Lean has mainly been used for digitizing theoretical mathematics…

The main goal of Lean 4 is to make Lean a good programming language, not just an evidence helper. The syntax has been redesigned in many ways to make it easier to write a wider range of programs. An optimizing compiler has been written that generates efficient C code. It has new high-performance memory management technologyhelps you avoid the problematic pauses during work that often accompany such tools (for example, garbage collection), and, if necessary, easily integrates with existing C / C ++ code. Lean is currently a largely self-contained language that is written in the Lean language itself.

To assess the suitability of Lean as a programming language for real systems, we decided to write a Lean implementation of a robotics controller running on a single board computer. To make the task more interesting, we chose a controller for a two-wheeled robotic platform. If Lean programs are unable to issue real-time commands to motors in response to sensor inputs, the system will literally crash.

Our goal was to create a working Lean controller. This is different from what people usually think of when using theorem provers. Typically, one can specify a formal controller model that can omit low-level details, define reflective axiom assumptions that are expected to be true for the environment, and then try to prove that the controller has stabilized the system in a world that satisfies the environmental axioms. This is a worthy goal, and we would like to eventually achieve it. However, since the actual implementation of the controller for this project will use the Lean language, we needed to include low-level details that might otherwise be omitted.

We started by buying a two-wheeled robot for $ 90 and began experimenting with Lean. We checked the generated C code and runtime library and found the code to be quite portable. Unfortunately, the pre-release of the Lean runtime library contains dependencies (for example, the libgmp library), and it is too large for an Arduino-based robot controller. Fortunately, the generated code is easy to run on a computer. Rasberry Pi…

We purchased the 8GB version to compile Lean directly in it. This added $ 80 to the cost of our project, and we fit into our required hardware constraints, and the Lean authors are interested in solving runtime library size issues.

The next step was to split the existing robotic controller code to run over a Bluetooth serial connection to run all the control algorithms on the Rasberry Pi while keeping the minimal code for controlling the motor and reading the accelerometer data on the Arduino board. It was quite simple, but required the use of Google Translate to understand the comments in the source code. You can see the source code after translating comments. here, and the sectioned Arduino code after extracting the control algorithms is here…

We then translated the control code from C to Lean using a manual but fairly straightforward process. Lean 4 ultimately creates functional definitions and has the precision, modularity, and compositional benefits of functional programming. However, it has a rich source language that allows for loops, mutable local variables, and structured flow control statements such as break and continue. Internally, Lean 4 uses a complex analysis process to automatically and transparently restructure code into functional definition. This reduced the level of effort required to port from C to Lean.

The Lean code we have written is available to the general public at Github… Basic step control function BalanceCar.update runs every 5ms. The Kalman filter is used to assess the orientation of the robot based on the gyroscope and accelerometer readings (6 DoF IMU). The PD controller takes the orientation state as input and determines the motor speed, thus closing the control loop.

After the porting was complete, we wrote some C code to connect the Lean control code to the serial Bluetooth APIs and tried it out. The initial results were entertaining, but not entirely correct:

This was a little disappointing, but it happens in real programming. We ran some tests, made some changes to reduce Bluetooth latency, and fixed a bug in the Lean code along the way. As a result, we have successfully created a working robot:

As noted earlier, this was just a small experiment to test Lean in a real-time controller and the work required to manually port code from C to Lean. We haven’t verified the correctness of the controller yet (yet), but when we have a little more time, we plan to work on it and integrate Lean controllers into the ROS ecosystem so that other people can try it out. We also have a larger project where the Haskell and Lean languages and the SMT solver are used together to create proven decompiler from 64-bit with x86 architecture to LLVM… We will have more information on this in the future.

All the work that we have done for this project, is in the public domainso that those who are interested in it can try it. We deliberately used a relatively inexpensive robot so people can easily try out the code. This way you can try out Lean in person or show students that you can write real programs in those languages. If you have any questions about the project, you can chat with us on the Lean Real-time Systems channel of the Zulip service.

I’d like to thank the Lean contributors who helped make this possible, and Joey Dodds for the comments that helped improve this post.

We have already written about how ML and computer vision are used in processing plants, and if you want to teach robots or machines to see the world, make decisions and act according to the situation, pay attention to our course “Machine Learning and Deep Learning” partner of which is Nvidia.

You can also take a look at profession C ++ developer, on which you can pump or learn C ++ from scratch. Come – it will be difficult, but interesting!