what is future of lean?

Stream: lean4

[Serhii Khoma (srghma)]

~5 months ago I made an issue (this issue is deleted bc I was blocked by github) at lean4 github

please make a javascript backend for lean4

and dont-remember-who (probably it was Sebastian Ullrich who responded)

no, we have many other more interesting plans for lean instead

so, I wanted to ask "what are these plans?"

[Bryan Gin-ge Chen]

Have you read the Lean FRO roadmap? https://lean-lang.org/fro/roadmap/1900-1-1-the-lean-fro-year-2-roadmap/

[(deleted)]

what do you mean by a JavaScript backend? that is Lean can produce JavaScript code?

[Serhii Khoma (srghma)]

Huỳnh Trần Khanh , Yes, bc purescript is not so powerful

P.S. or issue was not about js backend, but about "please rewrite kernel in lean itself instead of c++"

also, I wish lean supported linear types to allow more optimizations

[(deleted)]

my general stance is the Lean developers already have a lot on their plate. there are things that can be done through contributing to the surrounding ecosystem instead of Lean proper

[(deleted)]

as for linear types, Lean already has reference counting, isn't that enough

[Mr Proof]

A Javascript backend would be nice. It would get people to really think hard about optimisation. The lessons learned would then be applied back to the desktop version.

Plus having it run in the browser allows you to use good formatting libraries such as MathJax to show Latex equations.

(Yes, there is the web-version but being cloud based, what if you are in a jungle with no internet?)

While it would be nice to have the kernel it in pure Javascript so the code be inspectable I think this may be unfeasible. A compromise might be to run the kernel as WASM code. (The hard bit might be if it uses external libraries such as GMP for the large integers these also need to be compiled to WASM). And then interface that with pure Javascript for the interface.

Here is the kernel code: https://github.com/leanprover/lean4/tree/master/src/kernel in C if anyone wants to have a go. (Or maybe someone's already done this before?)

Downsides: You would have to store a copy of mathlib on your computer (but perhaps just the definitions).

@Bryan Gin-ge Chen Yes, I've read the roadmap. But (1) it is higher vague. e.g. "Scalability Enhancements" is an admirable goal but could mean anything. and (2) Things not on the roadmap could be projects for people to do for their own amusement. (Whether someone does something on the roadmap or not, they don't get paid either way!)

[Henrik Böving]

A Javascript backend would be nice. It would get people to really think hard about optimisation. The lessons learned would then be applied back to the desktop version.

people already really think hard about optimisation, there is no need for a javascript backend for that.

[Mr Proof]

@Henrik Böving Thinking about things and doing things are two different things. One may think very hard about prepping for a flood but when the waters are seeping through the gaps in your brickwork you get a better idea of where the problems are.

[Henrik Böving]

People are already doing performance optimizations as well, there have been dozens of commits to the code generator, there is the new module system for faster rebuilds together with incrementality and in-file parallelism, Leo has halfed the runtime of grind on some real world examples in the past two weeks, we have the best performing fully verified bitblaster that exists.

[Mr Proof]

OK. Did anyone say there hasn't been improvements? I don't understand why every comment about interesting projects to do or suggestions for improvements is taken as a personal attack on the dedication of people working on Lean?

We are VERY VERY grateful and HIGHLY appreciative of all the work you've been doing.

PLEASE PLEASE don't take comments or suggestions about things to be PERSONAL ATTACKS.

[Mr Proof]

I make computer games for a living. And when people give comments or suggestions. I think to myself. "Here is someone who didn't like the game" I may agree or not agree but it is all HELPFUL information.

[Mr Proof]

It is not an attack on my ego.

[Henrik Böving]

You said "Thinking about things and doing things are two different things" and I merely pointed out that indeed people are not just thinking but doing things.

[Johan Commelin]

Also, I think that

It would get people to really think hard about optimisation.

suggest that people are not yet doing that. To me "would get people to X" means that people are not yet doing X.
Maybe that's not what you intended... but I think it explains some of the push-back you are getting.

[Mr Proof]

Johan Commelin said:

Also, I think that

It would get people to really think hard about optimisation.

suggest that people are not yet doing that. To me "would get people to X" means that people are not yet doing X.
Maybe that's not what you intended... but I think it explains some of the push-back you are getting.

Yeah, well it's still highly unoptimized by usual software standards. So if people have a problem with me saying that, that's more of a "them" problem than my problem.

[Arthur Paulino]

We all have the freedom to be unsatisfied with software and hardware speed. It's your approach that's off.

Performance in a complex system such as Lean 4 has many dimensions and layers. So instead of simply saying that it's slow, I'd suggest a more structured way to communicate that at least displays some effort.

For example: "I'm trying to do X and it seems to be particularly slow. I tried to do X on this other system Y and it goes smoother. I looked at the source code and I found this call to Z, which I think is the bottleneck. On a local copy of the Lean 4 source code, I tweaked it a little bit and got a speed boost of P%. Is this approach dangerous in any sense?"

That would be the best approach I can think of. But if you just go with the first sentence and be very specific and explicit on X, that's already better than the opaque statements you're making.

[suhr]

Mr Proof said:

Yeah, well it's still highly unoptimized by usual software standards.

Would you like to name a faster proof assistant?

[suhr]

I believe Lean is faster than both Rocq and Isabelle/HOL.