Performance comparison between Lean and Ada

Stream: general

[Bulhwi Cha]

Forgive me for lacking expertise in programming language design and other related areas. As far as I know, Lean code is transpiled to C code, as explained below.

From https://lean-lang.org/doc/reference/latest//Elaboration-and-Compilation/#elaboration-results:

Finally, the compiler is invoked to translate the intermediate representation of functions stored in its environment extension into C code. A C file is produced for each Lean module; these are then compiled to native code using a bundled C compiler.

However, Lean uses garbage collection, so I guess its performance is generally worse than other languages using manual memory management.

According to "Introduction to Ada," Ada's performance is comparable to that of C. Then, does Ada perform better than Lean?

From https://learn.adacore.com/courses/Ada_For_The_Embedded_C_Developer/chapters/08_Performance.html:

All in all, there should not be significant performance differences between code written in Ada and code written in C, provided that they are semantically equivalent. Taking the current GNAT implementation and its GCC C counterpart for example, most of the code generation and optimization phases are shared between C and Ada — so there's not one compiler more efficient than the other. Furthermore, the two languages are fairly similar in the way they implement imperative semantics, in particular with regards to memory management or control flow. They should be equivalent on average.

[Robin Arnez]

It doesn't use garbage collection but reference counting with reset-reuse. Still, the performance is probably worse than in Ada because again, reference counting and because almost all types are stored on the heap and not on the stack (there are plans to change this though).

[Bulhwi Cha]

Thanks for the correction. I've recently become interested in Ada because there's a programming language called SPARK, which is based on a subset of Ada and is targeted at functional specification and static verification.

[Bulhwi Cha]

I think it'd be nice if we had a toolchain that translates Ada/SPARK programs to functional models in Lean. However, we already have Aeneas, and I suppose people are currently much more excited about Rust rather than Ada/SPARK.

[Steffen Reith]

We did some smaller projects with ADA/Spark a decade ago. It worked quite well and the measured performance was sometimes even better than C implementations. Unfortunately, ADA only became established within a narrow circle. Currently, I would rather rely on Rust and projects like Aeneas.

[Nina Chloé Kassi]

Bulhwi Cha said:

Thanks for the correction. I've recently become interested in Ada because there's a programming language called SPARK, which is based on a subset of Ada and is targeted at functional specification and static verification.

I'm also interested into Ada/Spark and thought about that some time ago too. Unfortunately, I am not anywhere close to familiar with lean4 to do something like that on my own.

[Andrés Goens]

Bulhwi Cha said:

Forgive me for lacking expertise in programming language design and other related areas. As far as I know, Lean code is transpiled to C code, as explained below.

Also worth noting that there is a new compiler incoming that doesn't compile to C (as far as I understand) and should have more control over stuff like unboxing certain types etc in the future, so the new compiler should also improve performance in the long run

[Robin Arnez]

The new compiler is already enabled and compiles to C; not sure about plans for switching to LLVM; iirc this was tested before though and the performance was worse with LLVM than going through C. Still unboxing is a plan, even if going through C to do so.

[Henrik Böving]

Andrés Goens said:

Bulhwi Cha said:

Forgive me for lacking expertise in programming language design and other related areas. As far as I know, Lean code is transpiled to C code, as explained below.

Also worth noting that there is a new compiler incoming that doesn't compile to C (as far as I understand) and should have more control over stuff like unboxing certain types etc in the future, so the new compiler should also improve performance in the long run

The LLVM backend has existed for years at this point, it's just not enabled by default because it is a few percent slower than C and we didn't figure out why at the time.

[Nina Chloé Kassi]

Bulhwi Cha said:

I think it'd be nice if we had a toolchain that translates Ada/SPARK programs to functional models in Lean. However, we already have Aeneas, and I suppose people are currently much more excited about Rust rather than Ada/SPARK.

More References are not that bad, I think. Do you think something like Aeneas for Ada could be of use?

I know Rust has a larger fanbase, but based on the vast amount of programming languages, I doubt, that there will be always that interest in Rust and Ada has some differences from Rust, that could be an actual advantage (e. g. Spark).

Also there is Why3 ( https://www.why3.org/ ) which is used within Spark. even if not directly interfacing Ada, interfacing with Why3 (supporting also languages like C) could be a base for Ada X lean4 programs / proofs, I think.

[François G. Dorais]

Henrik Böving said:

The LLVM backend has existed for years at this point, it's just not enabled by default because it is a few percent slower than C and we didn't figure out why at the time.

Does this imply that you have figured out why at this time?

[Henrik Böving]

No