Mysterious quote suggests that Lean is faster than Rust

Stream: general

[Oliver Butterley]

In the post about Cedar it is written that "Lean's fast execution time of only 5 microseconds per test case, compared to Rust's 7 microseconds per test case, makes this extensive testing practical." This appears to say that there are two implementations with equivalent properties, one in Lean and one in Rust and, when compiled, the Lean one is faster than the Rust one. This can't be true else they would just have used the version written in Lean for production and there are so many low level optimizations possible in Rust that one can produce code that runs much faster than compiling from Lean. Can anyone help me understand what I'm missing about this statement from the post?

[Markus Himmel]

Oliver Butterley said:

This can't be true else they would just have used the version written in Lean for production

There are many reasons besides speed to choose one language in production over another. For example your deployment pipeline or observability tools or other infrastructure might be limited to a given set of languages or build systems. My speculation would be that deploying a new technology to production at a company like AWS requires a lot of bureaucracy. Also, it's hard to deploy a microservice written in Lean without an HTTP server (we're working on that) unless you're willing to communicate via something like stdin/stdout or do reverse FFI, both of which come with their own pitfalls.

[Oliver Butterley]

Yes, you are right, there are many other motives behind the choice of the language used in the production software. I oversimplified. To correct my first comment: there are various suggestive details here which make me think that I have misunderstood the precise meaning of the quote.

In particular, is the Lean complier so good that it can compare on speed to well written Rust code? (Ignoring for the moment all the bit-level type optimizations which can be written in Rust code.)

[Oliver Butterley]

My best guess in this case is that the Rust code is doing much more than the Lean code which is being used to test it.

[Markus Himmel]

The most serious attempt at measuring Lean's performance that I am aware of is the benchmark section of the counting immutable beans paper (which is getting on in years, so it might be time to rerun some of these experiments). It shows that Lean is quite competitive with other GCed or reference counted languages (or at least it was six years ago).

The lack of GC/reference counting and fact that data structures in Rust (and C++) require fewer pointer indirections by default mean that it is certainly possible to write faster code in Rust/C++ than in Lean. The margin depends on the kind of problem you're solving, and also on how well-written your Rust code is. If your code is full of Arc and clone (and there are at least a few in the Cedar evaluator), then it's quite possible that this benefit evaporates because you're essentially adding reference counting and pointers back into your language.

On the flip side, the fact that it is possible to statically prove that array accesses are in-bounds gives Lean a theoretical advantage over Rust. When I wrote the code that later became docs#Std.TreeMap, I measured that replacing panic! with False.elim ... in the rebalancing routines of the binary search tree gave a speedup of a few percent in microbenchmarks because the compiler was able to remove the corresponding branches. If I write unreachable! in Rust, this is not possible, it has to perform the check at runtime. How much of this is visible when measuring the performance of entire programs remains to be seen.

Note also that Lean compiles to C which is compiled by clang, so there is a very sophisticated compiler under the hood for Lean as well in addition to the Lean compiler, which contains a decent number of optimization passes.

The truth is that it's really hard to take anything away from these kinds of cross-language benchmarks unless you're measuring the exact program you're intending to run.

[Oliver Butterley]

Thanks for all the very comprehensive comments!

I realise now the thread title I wrote was rather misleading, I'm sure that Rust has the advantage over Lean on speed, sometimes marginally faster but a massive advantage on really optimized code. I spend my time verifying Rust crytography code, extracting it with Aeneas and verifying in Lean (obviously including Rust code that uses beautiful tricks for fast computation). I'm convinced that working with the Rust -> Lean pipeline is worthwhile for multiple reasons, Rust will remain important in production software for a long time and Lean allows us to prove properties.

This thing which prompted me to ask here was that someone recently pointed to the Cedar quote of 5 versus 7 microseconds as evidence that Lean is faster than Rust and therefore there is no benefit to verifying Rust code in Lean, better to work directly in Lean. This was why I was trying to dig into the details behind the quote.

[Kyle Miller]

My read for this quote is not that it's pointing out that Lean is faster, but that the runtime is comparably fast, thus practical. The sentence still makes sense to me even if it had been "Lean's fast execution time of only 15 microseconds per test case, compared to Rust's 7 microseconds per test case, makes this extensive testing practical."

[Niels Voss]

Would using unreachable_unchecked! allow rust to recover the the performance advantage of Lean, at the cost of safety?