To what extent is Lean4 itself verified?

Stream: Program verification

[Philogy]

Hi, I'm studying Lean in the context of using it for program verification and developing mission-critical software using it. I'm curious what guarantees Lean provides about itself as a foundation, sure Lean checks my theorems and assertions but who is checking that Lean itself is checking things correctly?

I assume there must some ground level/kernel that must be assumed/audited to work correctly and everything is built ontop of that but what is that and where can I learn more about it?

Thanks!

[Chris Henson]

For some info on the kernel, you might start with this repo/book: https://github.com/ammkrn/type_checking_in_lean4

[Henrik Böving]

For one there is a theoretical soundness argument for Lean 3's logic in #leantt. Sebastian Ulrich's PhD thesis sketches how this work would change for Lean 4 (not a lot at all).

The kernel itself is a couple of thousand lines of C++ code. However it may be exchanged for other kernels so you can check your proofs with a multitude of checkers to see if they all agree.

[Philogy]

Chris Henson said:

For some info on the kernel, you might start with this repo/book: https://github.com/ammkrn/type_checking_in_lean4

Thanks will look into this!

[Philogy]

Henrik Böving said:

The kernel itself is a couple of thousand lines of C++ code. However it may be exchanged for other kernels so you can check your proofs with a multitude of checkers to see if they all agree.

Interesting, that seems quite small, good to know!

When you use Lean4 as an interactive theorem prover, interpreter or compiler do they all rely on the same kernel?

Also is the kernel actively part of Lean or is it simply the basis upon which Lean is bootstrapped before eventually fully being implemented in itself?

[Shreyas Srinivas]

The kernel is not a compiler. It is a typechecker. The way lean works is that type checking is outsourced to the kernel. The kernel has a somewhat minimal language. The rest of lean's proof infrastructure takes lean code that you see in a text editor and compiles it down to the kernel's langauge and asks whether that code + environment typechecks.

[Shreyas Srinivas]

You can mark somethings unsafe or partialif you don't want to prove that they are terminating and so on. Then these definitions cannot be used in terms which are checked by the kernel. It is a different matter that they can be compiled down to C and run. Sometimes you want to have the latitude to write unsafe procedures to produce proof terms for example.

[Mario Carneiro]

Henrik Böving said:

For one there is a theoretical soundness argument for Lean 3's logic in #dtt.

You meant to link #leantt

[Mario Carneiro]

Shreyas Srinivas said:

The way lean works is that type checking is outsourced to the kernel.

It's not really outsourced to the kernel, because the elaborator also has a typechecker, essentially independent of the kernel typechecker. But the kernel typechecker is a kind of backup plan in case there is a bug in the (much bigger and more likely to have bugs) elaborator, and it means that you don't have to trust the elaborator to believe the results.

[Mario Carneiro]

But I think the most relevant link for "is lean4 itself verified" is https://github.com/digama0/lean4lean (+paper), which is a project to verify the correctness of a lean 4 kernel implementation and formally prove the theorems from #leantt

[Eric Wieser]

Philogy said:

Hi, I'm studying Lean in the context of using it for program verification and developing mission-critical software using it.

I don't see this mentioned yet, so: if your goal is to actualy compile Lean code to mission-critical software, the compiler in Lean is not verified.

[François G. Dorais]

Shreyas Srinivas said:

You can mark somethings unsafe or partialif you don't want to prove that they are terminating and so on. Then these definitions cannot be used in terms which are checked by the kernel.

Actually, partial defs are completely edible by the kernel. However, you can't prove anything useful about these functions. As far as the kernel is concerned, these functions simply return a completely arbitrary and unspecified value of the given type. This is sound for type checking since it is required that the type is inhabited.

[Shreyas Srinivas]

I mean "outsourced" in the sense that one doesn't trust the elaborator as much as the kernel.

[Shreyas Srinivas]

and of course the environment needs to be checked in the end.