Lean's implementation

Stream: general

[crab]

also, what language was lean originally implemented in?

[Mario Carneiro]

C++

[crab]

Mario Carneiro said:

C++

why tho lol

[Mario Carneiro]

because leo knows C++ really well

[crab]

i would think that it was implementedin haskell or some functional lang

[Mario Carneiro]

They certainly felt the pain, that's why they rewrote it in some functional lang

[Mario Carneiro]

namely lean

[crab]

lean lol

[Mario Carneiro]

but it's hard to get the performance characteristics you want with functional languages

[crab]

i thought it is said that the programming language you use to make the compiler in doesnt really affect the speed

[Mario Carneiro]

lean 3 is being used in a very computationally heavy way, I can't imagine how many more CPU hours we would have burned on mathlib if the elaborator was less efficient

[crab]

i feel like rust is going to take over c++ for lang dev imo

[Mario Carneiro]

The programming language you use to make the compiler certainly affects the speed of the compiler

[crab]

c++ doesnt even have pattern matching

[Mario Carneiro]

and in theorem proving you spend all your time in "compilation"

[Eric Wieser]

(I split this thread in case anyone has something to add to the logo conversation which we seem to have diverted from)

[crab]

Mario Carneiro said:

The programming language you use to make the compiler certainly affects the speed of the compiler

well, maybe the first implementation. for instance, rust was originally written in ocaml, but then rewritten in rust, and is now one of the fastest langs

[crab]

explain that

[Mario Carneiro]

Well, lean hasn't been self hosting prior to lean 4

[Mario Carneiro]

plus, that's only a good strategy for improving the compiler if your programming language is actually faster than the original language. Rust can definitely beat OCaml in some domains. I think it will be hard for Lean to compete with C++ on speed, but certainly there are some aspects that were being done inefficiently in C++ just because the setup is so much boilerplate work (e.g. everything was an expr because making inductive types in C++ is incredibly painful)

[crab]

im just showing

[crab]

that the programing lang you use doesnt affect the speed of the compiler nessacerily

[Mario Carneiro]

For a self hosting compiler, the speed of the compiler depends on how good it is. Good compilers are a ton of work

[crab]

right

[crab]

that is what matters

[crab]

rust was a good compiler

[Mario Carneiro]

Rust eventually became a good compiler after a ton of work

[Mario Carneiro]

Every compiler is born crappy

[Mario Carneiro]

and it's really hard to compete with e.g. LLVM, which is why even rust doesn't go there

[crab]

Mario Carneiro said:

Every compiler is born crappy

im gonna be honest, when rust first started, it was shitty like hell

[Mario Carneiro]

You realize that there is 1 or 2 orders of magnitude between the rust community and the lean community, right?

[crab]

im not saying lean is shitty

[Mario Carneiro]

We're doing our best to scale up but all theorem prover langs are in the rounding error compared to regular programming languages

[crab]

tbh, the rust community is really huge

[Mario Carneiro]

I don't think that speed is the main reason for self-hosting lean 4. It's more about the expressiveness and enabling user code to interact directly with the elaborator

[Mario Carneiro]

It's going to hugely speed up mathlib compilation, but that's because we're able to compile tactics now. It was too much work and too organizationally complicated to write tactics in C++, so most tactics were written in lean and interpreted. So Lean 4 is competing with (and beating the pants off) the lean 3 interpreter, not C++

[Kyle Miller]

It also opens up being able to give Lean proofs that different parts of Lean written in Lean operate correctly, which is cool (at least in theory -- don't know if anyone is planning on doing this).

[Mario Carneiro]

I think there are still a number of challenges to solve before that becomes theoretically possible. Most of the elaborator is in a lifted IO monad

[Mario Carneiro]

and partial and extern make everything interesting

[Mario Carneiro]

but hats off to the lean team for making almost everything be non-unsafe, so at least it's logically consistent for those functions to exist

[Mario Carneiro]

by contrast to lean 3 where everything is meta (= unsafe)