Compilation via theorem proving

Stream: lean4

[Michal Šustr]

Hi all!

First, a motivation: Popular programming languages, such as C++ or Rust, use compilers to produce low-level intermediate representation of code, which is passed to LLVM and subsequently final assembly is produced.
While many local heuristic optimizations have been implemented over decades by experts, end-to-end optimization of code translation is only a recent topic, and typically limited in scope (ie optimize computational graphs of neural networks for GPUs)

Here comes the connection to Lean: if you treat assembly operations as "axioms" in your logical system, and build language on top of them, you could use theorem proving to compile the code (ie take advantage of the curry-howard isomorphism). Compilation can be than cast as theorem proving to axioms / assembly, and optimization is finding the shortest proof.

However, the Lean core is implemented in C++, not Lean. Are there some projects that go in this direction that could help reformulate programs as theorems?

[Niels Voss]

What do you mean by "Lean core"? From my understanding, the Lean compiler and standard library is written predominantly in Lean itself, with mainly the kernel and optimized representations of some types (e.g. Array) being written in C++.

[Robin Arnez]

One small correction: the old/currently used compiler is indeed in C++ but there is a new compiler in the works that is written in Lean.

[Mario Carneiro]

the old compiler is only half in C++, everything from the IR down to printing strings of C code is in lean

[fishooter]

everything from the IR down to printing strings of C code is in lean

Very interesting, thanks!

there is a new compiler in the works that is written in Lean.

Is this for Lean 4, or would that be in a new version of the language?

[Kevin Buzzard]

This is for lean 4.