Just curious. Has anyone looked more deeply at this.

https://tarides.com/blog/2022-12-27-love-rust-then-ocaml-s-new-eio-library-is-for-you

It claims ocaml with the speed of rust (minus 3%). So, one could naively dream about Coq at the speed of lean.

is lean fast?

circa end of 2021, it wasn't, but maybe this has changed with Lean4 milestones? https://leanprover-community.github.io/blog/posts/backstage-with-dillies/

Another thing is that Lean is slow. I notice that I have an upper bound on my coding speed because it takes a while before Lean updates the goal. And it's really painful when you have to wait 3 seconds at each keystroke. Had it been faster, I could have done some random thing in 10 minutes, but I spent 1h30 instead. And this happens for several reasons: long proofs and long files. If Lean could provide support for more granular recompilation of long proofs, that would be great. By now, many of the large files have been split into smaller pieces, and I am working on some of the remaining ones.

of course "slow" and "fast" changes with the benchmark, and UI issues may play a role in the quote

I remember, at some point is was claimed to be fast, as it was written in C++, but I've never done any comparison myself.

Lean4 to my knowledge is mostly implemented in Lean(4)

it would be nice to have a benchmark suite for the "same" big definitions/proofs in comparable systems, e.g., Agda/Coq/Lean. But chance of getting research funding to develop this is probably around zero.

Typeclass resolution / unification are specific examples that come to mind on what to [performance] test.

That blog posts has strong hints that it's about async code for highly concurrent servers

I once tried to see if anyone had even done a proper software engineering style performance comparison of name binding approaches. Couldn't find any, e.g., de Bruijn only vs. locally nameless on huge terms

Not in the context of proof assistants per se, but Stephanie Weirich has done this experiment to try to benchmark capture avoiding substitution implemented in various ways (after an earlier similar experiment by Lennart Augustsson):

https://github.com/sweirich/lambda-n-ways

@Bas Spitters this seems to be a library for IO, which is not the main throttle of Coq processes. Coq is heavily memory-bound, not IO-bound, so this probably wouldn't change anything.

Also, re: lean, I discovered recently that the Lean kernel uses a naive reduction machine (read: O(n) eager substitution) so there is no way this can be fast on non-trivial conversion problems. It seems that the mathlib style works around these issues by relying on HOL-style proofs, but still.

@Pierre-Marie Pédrot Thanks! I may have misread, but I understood that this is about concurrency. Your arguments will likely still apply.

It's build on ocaml 5. I know that ocaml 5.0 slowed down coq, quite a bit. I believe this has been resolved now, but you'll certainly know more than I do.

My five cents: I am usually *very* impressed by the speed of Coq. With reflexive tactics it can do quite complicated proofs in a fraction of a second.

Last updated: May 24 2024 at 22:02 UTC