general-purpose programming

Stream: lean4

[Arthur Paulino]

I've seen/heard from multiple sources that there's a plan for Lean 4 to be a general-purpose programming language. Is there something like a plan of action or roadmap?

[Arthur Paulino]

I'm curious because there are strong languages out there like clojure/javascript/python/go

[Henrik Böving]

Leo said in a past topic, I can't remember right now, that at the moment the top priority for the Lean 4 project is to get mathlib4 (the mathlib port from Lean 3 to Lean 4) fully up and running. After this is done they'll clean up the compiler etc. but he expects this to only fully finish somewhere towards the end of 2022.

That being said Lean4 can be used for regular real world programming right now, I've for example written a university assignment with https://github.com/xubaiw/lean4-socket by @Xubai Wang who has also done some other general purpose lean things on his github (csv, termios). I have also written a tiny bit of Lean 4 that interacts with C code here https://github.com/hargoniX/lean4-statvfs, the Lean 4 compiler itself is largely written in Lean 4, the Lake build system (https://github.com/leanprover/lake) is etc. So it is definitely possible right now to link Lean 4 code against real world C APIs and start building whatever you want with it, it's just that no one has built all the things you would usually expect from general purpose programming languages regarding interaction with the rest of the world yet.

And performance wise there are actually reasons to use Lean 4 as a real world language over other functional ones, the modified reference counting (you can check up on that in the "counting immutable beans" and the "perceus" papers) allow Lean to outperform other well established functional languages such as OCaml or Haskell and for example the "sealing pointer-based optimizations behind pure functions" paper shows that dependent type theory actually allows us to build things in pure functional languages that weren't possible without it.

So TLDR, it's already very much possible from a language point of view, it is "just" that someone has to actually implement all the things other languages use when interacting with the real world to build real world stuff.

[František Silváši]

I happen to be writing a WebSocket server in Lean4 also using the aforementioned lean4-socket library. While it is not available just yet, the protocol necessitates existence of sha1 which I already made public. The ecosystem for "programming" is currently in its infancy but Lean4 is by a great margin a programming language I find most enjoyable using. Thanks @Xubai Wang for the socket implementation!

[Henrik Böving]

Cryptography code is also a topic I imagine could be very interesting in Lean? Maybe it could be possible to somehow proof that certain functions are constant time operations, providing additional guarantees...then again regular lean code will most likely not be able to outperform handwritten C stuff like openssl or libsodium so at some point someone will have to write an FFI interface to those.

[Arthur Paulino]

And communication with popular databases like MySQL and PostgreSQL.
A Spark API would be big I think.

[František Silváši]

I'd rather cryptographic code was safe than fast! :) It's not outside of the realm of possibility to have a formalized representation of (a subset of?) C which you use to state equivalence between a function in Lean and its implementedBy C counterpart. Then you use CompCert to have confidence in the compilation process of C and then you hope that hardware it's running on works as advertised. Of course, this is far from a trivial undertaking.

[Kevin Buzzard]

@Kyle Miller wrote a raytracer in Lean, the guys at Galois wrote a program which kept a wheeled robot standing up, and someone wrote a Mandelbrot set program. Do these count? I've tweeted links to all these things in the past but I'm not 100% convinced that this is what the question is about and searching Twitter is hard :-/ (or I don't know the tricks...)

[Arthur Paulino]

Hm, I was talking more about common software engineering challenges in the industry, like backend/frontend development or data analysis

[Arthur Paulino]

Right now I'm going through the challenge of learning Lean 4 and trying to make a Lean package that can talk to MySQL. This is, however, a rather slow process. But I'm enjoying it

[Johan Commelin]

Certainly a raytracer and a robotics application must be legit instances of "general-purpose programming".

[Arthur Paulino]

Definitely. I'm 100% convinced that it can be done. And there's so much stuff to be built.

[Tomas Skrivan]

I also want to use Lean 4 as a general purpose language. I'm attempting to write a library to allow you to do computations like in Mathematica/Julia/NumPy/SciPy. It is still in a very early stage but I already have a reasonable automatic/symbolic differentiation code. Hopefully, I will get it into a reasonable state in a month or two so I can share it with others.

[Arthur Paulino]

That'd be dope!

[James King]

I'm working on examples for the Lean 4 hacker guide that implement common Unix-like tools -- suggestions welcome. :)