Making Lean 4 compiler more functional and monolith

Stream: lean4

[Guilherme Silva]

Lean 4 in its core is already functional and made in Lean 4.
The problem is in the front-end and backend.

In the front-end, because Lean 4 is made to work using LSP, some of the code is written in TypeScript or JavaScript.
Programming languages such as Hazel are made using a reactive programming language framework (ReasonML in OCaml).

In the backend, I think that the CakeML approach is one of the best. They implemented a silver CPU in HOL.

I don't know how hard is to implement both of them in Lean, but I would like to know if there is something being made in this direction.

[Daniel Fabian]

FWIW, the front-end is really mostly not implemented in the front-end. The typescript part is a thin wrapper around messages that are created in the lean 4 core.

[Guilherme Silva]

I think that in Lean 3, they developed a small framework to use Lean code in VS Code.

Maybe, with one framework like that, this typescript wrapper will no longer be necessary.

[Chris B]

Guilherme Silva said:

The problem is in the front-end and backend.

What is the "problem in the front end and backend"? VScode requires users to write their extensions (or at least the part that touches VScode) in typescript.

Guilherme Silva said:

In the backend, I think that the CakeML approach is one of the best. They implemented a silver CPU in HOL.

The best at what? I'm sure it's very cool, but a custom ISA for a specific model of FPGA doesn't sound super practical.

[Guilherme Silva]

A formal model of the processor can help to have fewer bugs, to debug and test the binary code generated.
Another advantage is to make verified optimizations.

[Chris B]

I don't think there's anything stopping someone from writing a verified compiler for Lean (other than it being a moving target for now), but the developers have said they're not interested in doing it themselves, or at least Leo de Moura has. Mario Carneiro's metamath zero is going after this level of depth, you might find it appealing: https://github.com/digama0/mm0.

[Daniel Fabian]

the target is far less moving if you look at kernel terms. There are multiple type checkers for it. And all the fancy stuff happens in lean syntax, elaboration, etc. The kernel is not changing when the language changes.

[Yuri de Wit]

FWIW, while watching https://www.youtube.com/watch?v=3ixaLQQNCFk I couldnt stop thinking whether WebAssembly, having a formally defined semantic and being language independent (among many other interesting properties), could be a great compilation target for Lean.

[Jason Rute]

By the way, with the mention of @Mario Carneiro's MM0 project, if I understand it correctly, it would be able to serve as a verified (external) type checker for any kernel-level proof in any theorem prover's logic, including Lean's. The idea being as follows:

• One writes a specification file, which is short, human-readable, and machine-readable, which details the rules of the logical system.
• One converts the kernel proof into an MM0 format which has two parts: (a) A human and machine readable part which includes the (elaborated) definitions and theorem statements. (b) A machine readable part containing the kernel proofs.
• MM0 checks a kernel proof against that specification.
• MM0 also has (or will have) a proof that the byte code of its checker will follow the specification given to it.
• Therefore if the specification is correct (checked by a human), the definitions and theorems are translated correctly to the MM0 format (checked by a human), and Mario finishes verifying the verifier, then the byte code (barring hardware errors) will correctly check the proof.

(Someone can correct me if I'm wrong on the details here.)

[Jason Rute]

Also, whenever someone mentions verifying a theorem prover, I feel compelled to mention that there are actually two ways to verify a theorem prover:

1. Verify that the checker follows the rules of the logic.
2. Verify that the rules of the logic are consistent (including any axioms used).

MM0's goal as I understand is the first, but it could in theory also be used for the second.

[Mario Carneiro]

Yes, you could use MM0 for metatheory reasoning, but that's not a current goal. Full proof translations often make metatheory reasoning more accessible, however, since it is only a minor tweak to the exporter to produce theorems in a deep embedding, and then you can prove general theorems about things in the deep embedding like soundness.