Lean project ideas for general-purpose programming

Stream: general

[Gavin Zhao]

I feel like the aspect of Lean as a general-purpose programming language is often neglected, hence this topic. Basically #general > dreams of big projects, but focused on the programming side instead of proof-assistant side in Lean, perhaps doing it dependently while we're at it.

[Gavin Zhao]

The ability to send HTTP requests is a must. From my observation, people are mostly shelling out to curl or similar command-line tools. @Sofia Rodrigues has a Std.HTTP client implementation at https://github.com/leanprover/lean4/pull/10478

[Gavin Zhao]

However I don't think that enables sending HTTPS requests. To do that purely in Lean, someone has to either:

• Write bindings to OpenSSL/MbedTLS/similar libraries to handle the encryption.
• Write a pure Lean implementation of such encryption.

[Gavin Zhao]

I recall seeing in multiple topics that there's demand for tools to automatically generate Lean bindings from C headers, so projects similar to cbindgen are likely wanted. One problem is that the Lean FFI seems to be still unstable, but if it's automated then probably changes to the FFI would not be that of a pain?

[Henrik Böving]

Write a pure Lean implementation of such encryption.

Please do not do this with the intent of having it being used as a real world library. Lean is not a good language to implement side channel proof crypto libraries in. If you really want to do it from within Lean it should be done from a DSL within Lean that directly generates C code (or similar).

Even though OpenSSL is well known for it's absolutely awful API it has a lot of things figured out correctly internally and we should not try to replicate them unless we have a good reason and people that actually know what they are doing in the space.

[Henrik Böving]

One important thing to keep in mind with the OpenSSL FFI is that you likely do not want the Lean library to ship its own OpenSSL dynamic library but to be able to link against the system library. This is so vendors can easily roll out bug fixes when they happen without having to touch every piece of software on their system. This poses an interesting challenge for FFI applications because suddenly linking against just one specific version of a header is not enough anymore, you actually need to be able to link against several different versions of the same library.

For this reason the lowest level crate in Rust that provides the direct FFI layer openssl-sys is in fact mostly hand written with a ton of configuration operations and ifdefs sprinkled throughout it. So while a first shot at an OpenSSL FFI could indeed be auto generated using something like bindgen in Lean, if we want it to stick to this principle of linking against the OpenSSL version your user wants instead of against the version you think is correct, a lot of it will have to be hand written.

That said I think a version of cbindgen could still be useful for linking against other C libraries regardless,

[cmlsharp]

Henrik Böving said:

Write a pure Lean implementation of such encryption.

Please do not do this with the intent of having it being used as a real world library. Lean is not a good language to implement side channel proof crypto libraries in. If you really want to do it from within Lean it should be done from a DSL within Lean that directly generates C code (or similar).

Even though OpenSSL is well known for it's absolutely awful API it has a lot of things figured out correctly internally and we should not try to replicate them unless we have a good reason and people that actually know what they are doing in the space.

FWIW the general state of language support for side-channel proof crypto is pretty bad (for example LLVM still has no support for semantically “secret” values and will sometimes insert branches even in seemingly branchless code. Trying to prevent it from doing this is a constant battle and the terrain can change under you at any time. At this point there’s really no substitute for freezing the compiler, putting all your sensitive code in inline(never) functions and checking the assembly output). And of course this is without even considering hardware.

(Here’s a really great paper on the subject https://eprint.iacr.org/2025/435.pdf).

Im not contradicting you really to be clear, just pointing out that this stuff is really complicated even without anything Lean-specific

[Henrik Böving]

I'm aware of the research surrounding this topic yes^^ I just think we should not try to play in this field unless we actually have people that have the skills to do it.

[Henrik Böving]

Or maybe we just rebuild perlasm in Lean :upside_down:

[Anthony Wang]

Gavin Zhao said:

However I don't think that enables sending HTTPS requests. To do that purely in Lean, someone has to either:

• Write bindings to OpenSSL/MbedTLS/similar libraries to handle the encryption.
• Write a pure Lean implementation of such encryption.

There's leanCurl which I've successfully used for HTTPS in a few small programs such as this one.

[Alfredo Moreira-Rosa]

i'm working on OpenSSL bindings for lean. i've done many in my carrier for other languages.
I'll give some updates when i can share some results. I'll support system library bindings, but unlike Rust bindings, i'll support bindings starting from version 3 and onwards. So not so much crazy if version checking in the library bindings internals.

[Kim Morrison]

@Sofia Rodrigues is also planning to work on OpenSSL bindings, and I'm sure will be interested in your work, @Alfredo Moreira-Rosa.

[Greg Shuflin]

I've been building off of the existing sdl3 bindings for Lean to try to create graphical programs with it (see #general > Fun with SDL3 )

[Greg Shuflin]

Another idea that I've had - some kind of parser generator that can prove that it parses exactly the context-free-grammar it is supposed to