System programming using Lean 4

Stream: lean4

[Ryan Lahfa]

For school reasons, I am looking to make a (micro|uni)-kernel in some language supporting formal verification, I know some Lean 3 and I was wondering if it was a good idea to jump into Lean 4 and try to make it into Lean 4, it looks like it might be able to fit the bill, I wonder how feasible this is?

e.g. how much stuff has to be reimplemented in baremetal to kickstart Lean 4 programs without any operating system on x86_64 for example? Is it easy or like insanely difficult?

[Ryan Lahfa]

I know the existence of stuff like https://github.com/stepcut/idrOS and am ready to carry out similar stuff if required

[Mario Carneiro]

There are commands that let you write bindings to C calls, so as long as C can do it I think it's possible to make lean do it

[Mario Carneiro]

I'm not sure how include files work though

[Ryan Lahfa]

I can indeed write down the required stuff to provide primitives in C, then if I can call them from Lean world and write down a model of they should work (which would be really cool if it stops at some boundary to define)

Also, maybe harder question, can Lean 4 compile to non-x86_64 platforms, e.g. RISC-V or ARM?

[Mario Carneiro]

If lean.h doesn't work because the baremetal environment doesn't have the support this might be a trickier task though. In particular I can imagine memory allocation being a sticking point

[Mario Carneiro]

lean compiles to C which compiles via any C compiler. So yes, it should work on any arch

[Ryan Lahfa]

Mario Carneiro said:

lean compiles to C which compiles via any C compiler. So yes, it should work on any arch

Wow! That's really neat :>

[Ryan Lahfa]

Hm, it looks like that I would need to patch this: https://github.com/leanprover/lean4/blob/master/src/runtime/object.cpp and everything else would reuse those implementations but I might be wrong?

[Mario Carneiro]

wait, that's C++ code? I thought the runtime was all C

[Ryan Lahfa]

Well, it is ; but as it looks like to be wrapped in some FFI, I imagine that I can just replace the cool STL containers & stuff by baremetal ol'C

[Ryan Lahfa]

I wonder if I can do unikernels of Lean 4 programs :D

[Wojciech Nawrocki]

@Ryan Lahfa I do not wish to discourage you, by all means do try to put Lean on bare metal! But it does seem like a Lean 4 OS would be a work-intensive project. While it is true that Lean programs compile to C which you could then compile to any architecture, they also link against the language runtime. So while you can definitely compile to RISC-V or ARM (with some obvious rough edges, but nothing should be fundamentally difficult), this is RISC-V or ARM with an OS. Being a reference-counted language, Lean needs the allocator in its runtime to function. So as Mario mentioned, you would need a heap, which is quite a few chapters into "Writing an OS in Rust". By contrast, there is an allocation-less subset of Rust which is used in that guide to get off the ground fairly quickly with displaying some text into VGA. On top of all this, numerical Lean code uses libgmp providing which in real mode sounds.. challenging. It sounds like you would have to cut that out of the runtime also. While I know nothing about Idris internals, looking at the idrOS project you linked it seems its author has written about 9k lines of C and 9 lines of Idris and then given up, so make of that what you will. Having said all this, I think it should be possible, it might just require a fairly high level of determination.

[Calvin Lee]

Wojciech Nawrocki @Ryan Lahfa Very much agree, having written an OS in Rust. I've been thinking about this idea a lot too. There are many parts of a kernel where heap allocation really shouldn't happen, or where data must be placed in certain places. Doing a unikernel should be a lot easier IMO, since you could write the whole runtime/OS in C/Rust and then use it in Lean.
Maybe if there were a way to make the typechecker linear so allocation wouldn't be necessary this could work.

[Calvin Lee]

Another issue I think you'd run into here is stack space.
Operating systems have notoriously tiny stacks (in some places, like the kernel stack for a process), usually just one page.
I know some OSdevs who have long, recursive functions, and if they recurse too much they have to be offloaded into new threads as to not overflow the stack. Really the rule of thumb is to never have your callstack over 5 layers deep.
On the other hand, I've had __huge__ issues with lean recursing too much. I've started to compile the program I'm writing with LEANC_OPTS="-fsplit-stack " so it can't overflow... and obviously this isn't possible in an OS context.

[Ryan Lahfa]

@Wojciech Nawrocki @Calvin Lee Well, it definitely makes sense to me ; I'm just wondering what is the shortest path to get something like a unikernel for example and what properties could I get from writing the rest in Lean 4, etc.
That's more an experiment than something else, my fallback project being writing the project in Rust with some design by contracts lib.

[Joe Hendrix]

@Ryan Lahfa An OS in Lean 4 sounds awesome. A practical consideration that Wojciech also mentioned is the Lean runtime is still pretty big. In particular it depends on GMP, and it introduces a bunch of dependencies due to the way constants are compiled. Essentially, you end up pulling a lot of the definitions needed for implementing Lean in the runtime dependencies.
We've gotten Lean 4 programs compiling and running as a process on a Rasberry Pi, but I think a more resource constrained environment would be a lot of work. Leo has heard about our experience at Galois, but I don't know how much of a priority it is to minimize the runtime and enable more bare-metal applications. I'd like to be able to compile Lean 4 code to Arduino eventually.

[Leonardo de Moura]

@Joe Hendrix We are currently fixing bugs and writing papers, but we hope to get back to the compiler in April. This issue is a priority.

[Christian Pehle]

I would distinguish between writing an OS and getting C++ to run on bare metal. The latter is relatively easy to do if you have a reasonably powerful embedded system as a target. All you need to get started is a bare metal build of gcc, an embedded C library like https://sourceware.org/newlib/, a linker script and a small set of c++ specific assembly routines. You need surprisingly little to get C++ running, see for example https://github.com/electronicvisions/libnux/blob/master/src/crt.s. So before trying your hand at compiling lean, I would start out just setting up an environment that allows you to compile C++ to bare metal on the platform of your choice.

[Ryan Lahfa]

We already done such things on RISC-V and FPGAs, so that's why we're interested into the next steps