Writing Production Software

Stream: new members

[Luka Hadžiegrić]

Hello! New to lean (and zulip). I'm kid of a hobby proover and functional programmer. I also started studying HoTT recently, little by little. Having previous experience with Agda and Haskell, how does Lean compare to them (and maybe Idris) in terms of writing software?

I've found Agda to be quite underwhelming in the area of writing "production" software, but that's to be expected as it is not the focus. Idris is improving, still not at the satisfactory level but getting there. Haskell is what I mostly use.

I've noticed Lean "advertising" as functional programming language which can be used as the theorem prover, but I get the feeling it has more focus on theorem proving. Am I right?

Writing "production" software that is also proven to be correct in the same language seems quite nice appealing to me. How far (or close) is Lean to that ideal?

[Johan Commelin]

@Luka Hadžiegrić welcome. You certainly want to look at Lean 4 (see also the #lean4 stream here on zulip).

[Johan Commelin]

Lean 3 is what most of us use, because Lean 4 is still brand new, and doesn't have a large maths library yet. Lean 3 is very good for theorem proving, but for practical production programming, my understanding is that Lean 4 is several miles ahead of Lean 3 (-;

[Johan Commelin]

I should add that I don't have any experience writing software.

[Luka Hadžiegrić]

That's cool, I've just been looking at that. Shame that all the info is still in the relative terms to the Lean itself e.g. Lean4 is faster than Lean3.

[Johan Commelin]

See also:
Marc Huisinga said:

The Lean 4 Theorem Prover and Programming Language

[Chris B]

There are some narrow benchmarks (data structures) with comparisons to other functional languages in this paper. https://arxiv.org/abs/1908.05647

[Chris B]

There's also Mario's metamath verifier: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Metamath.20verifier.20in.20Lean.204/near/237837021

Which apparently performs very well compared to the C implementation.

[Luka Hadžiegrić]

Yes, this seems impressive. I wonder if there are any web server libraries for Lean already? Seems like they have opened up quit a few possibilities for memory management performance in that arxiv paper.

[Huỳnh Trần Khanh]

Not yet. The Lean 4 ecosystem is virtually nonexistent. You can't write production quality software with Lean yet, unfortunately. Theorem proving software is, for the most part, experimental.

[Kevin Buzzard]

This is a very ill-informed comment. There have been some major pieces of software verification done in Coq.

[Huỳnh Trần Khanh]

Thanks. I crossed out the ill-informed part :smile:

[Kevin Buzzard]

I agree about the Lean part, but Lean 4 was only released this year. The ecosystem will emerge.

[Wojciech Nawrocki]

Luka Hadžiegrić said:

Yes, this seems impressive. I wonder if there are any web server libraries for Lean already? Seems like they have opened up quit a few possibilities for memory management performance in that arxiv paper.

Technically there is a demo webserver :) Of course it is very simple, but demonstrates cool syntactic features.

[Huỳnh Trần Khanh]

Well, for HTTP you can get away with a homebrew implementation. Because you have to use a reverse proxy to manage more complicated aspects of HTTP anyway, such as TLS, HTTP/2, virtual hosts, etc :joy:

[Huỳnh Trần Khanh]

Your stuff might not be production quality, but it doesn't hurt to try. :clown: