FYI: Thoughts on a broader Julia (Lean?) usage

Stream: lean4

[Yuri de Wit]

Watch JuliaCon 2022 Keynote (https://youtu.be/s6pjxCuNGjc) by Jeremy Howard.

Some interesting thoughts that may be useful to help Lean grow as a Language and ecosystem.

[Tomas Skrivan]

What do you think will be the main challenges for Lean to gain wider popularity?

I see there might be problems with:

• lack of libraries: this is a problem for any starting language
• overselling verification: people already interested in verification are already using Lean, Coq, Agda, ... They are small in number and just need to be convinced to switch to Lean. In my opinion, Lean is wonderful language even if you are not interested in proofs.
• do notation and monadic programing: if you are not a Haskell programmer the do notation is a bit strange. Similar to Haskell, the is a potential that the doc/libraries will be littered with math mumbo jumbo impenetrable for normal people.
• custom syntax: I love the extensibility of Lean's syntax. However, I can see how every library creator will go nuts, define their own DSL, and using Lean will effectively requite learning dozens of poorly documented languages.

[Tom]

I think debugging is high up there, and one of the important historical problems with Julia.

[Mac]

Tomas Skrivan said:

What do you think will be the main challenges for Lean to gain wider popularity?
[...]

• custom syntax: I love the extensibility of Lean's syntax. However, I can see how every library creator will go nuts, define their own DSL, and using Lean will effectively requite learning dozens of poorly documented languages.

While I agree with your other points, I think this point is a common concern that I doubt will be as bad as people think. Lean has very good editor integration for its custom syntax (highlighting, hovers, go-to-def, docstrings), so much so that I think using custom syntax will become second nature just like using functions, subroutines, objects, and classes are at the moment (all of which were rather revolutionary when they were first introduced).

Custom syntax also has the potential advantage to allow the expression of concepts in a way that is more natural to the topic in question, which can often improve readability over bare-metal functions. Thus, it may turn out that poorly documented code using custom syntax is actually easier to understand than equivalent poorly documented functions. Admittedly though, if the syntax of the topic is too esoteric, it may conversely become harder for people unfamiliar with the subject to understand even if it is easier for those more familiar.

[Arthur Paulino]

This is something I've already mentioned to Leo in a conversation we had... I believe that languages can get extra traction with examples of problems/solutions that require involved code in most situations but are solved with brevity and elegance in the language in question.

My background is the traditional software engineering industry, where people use JavaScript, Python, C++, Java etc. And in my experience, Lean 4 has helped me with issues that would have given me way more headaches in other languages.

But I don't know enough to tell where Lean is wrt other FP languages like Haskell or Clojure. The ecosystem is still small, but that's the obvious answer.

Also, I know, for instance, that people are deploying verified code with Coq + code extraction out there. What does Lean 4 offer to facilitate the life of those people? And I believe that they'll ask for more fundamental improvements besides the easiness of cutting off the extraction step

[Henrik Böving]

Regarding the Coq part, right now not really much, the Coq proving eco system is huge, if these people wanna maintain their level of research and not rewrite the proof libraries there already are for program verification they have no reason to look at Lean at the moment really.

[Mac]

@Henrik Böving I wonder if it would be feasible to embed Coq in Lean?

[Mac]

That way Lean could use all (or at least many( of Coq's packages.

[Henrik Böving]

The type theories are certainly very close and I believe someone somewhere already made a Lean -> Coq thingy let me try to dig it out

[Henrik Böving]

https://coq.discourse.group/t/alpha-announcement-coq-is-a-lean-typechecker/581 there it is

[Henrik Böving]

So yeah...sounds possible to me although I would have no clue where to start

[Mario Carneiro]

This is a... complicated question, and the simple answer is that if you want a fully proof preserving shallow translation then no it's not possible in either direction. That post has to turn off a lot of coq kernel checks (including some that are critical for soundness) to make the proofs go through

[Mario Carneiro]

You can get an approximate translation for most of the language though

[Mario Carneiro]

A mathport style source-to-source translation from coq would be really cool and much more useful I think

[Mac]

Mario Carneiro said:

A mathport style source-to-source translation from coq would be really cool and much more useful I think

Yeah, this was more of what I was suggesting. However, my though was more along the lines of a DSL than a single pass transpilation.

[Tomas Skrivan]

Mac said:

While I agree with your other points, I think this point is a common concern that I doubt will be as bad as people think....

Very good point, I'm quite curious how it will turn out.

My latest unpleasant experience was when you updated Lake's DSL. I needed to specify particular revision withrequire and I missed the @"rev" in the example, it is burried in the middle of a very long command. I was confused for couple of minutes and I tried few random things before I got it working.
If the dependency would be specified with a structure, code completion would guide me on how to set it up. Maybe I just need to learn how to use editor go-to for custom syntax.

[Mac]

Tomas Skrivan said:

If the dependency would be specified with a structure, code completion would guide me on how to set it up.

How so? There is code completion for structures? I have never seen that while coding Lean thus far.

[Tomas Skrivan]

Sorry, it might not be code completion per se, but I could easily look up the structure definition with go-to. I expect that there would be an inductive type to specify dependency location with constructors for GitHub repo, local folder, ... And there the code completion would help me.

[Tomas Skrivan]

Quite ofthen when I run go-to on some custom syntax it takes me to some code about generic elaboration in the main Lean codebase.

[Sebastian Ullrich]

But also, we should definitely implement completion inside structure instances

[Wojciech Nawrocki]

If the dependency would be specified with a structure, code completion would guide me on how to set it up. Maybe I just need to learn how to use editor go-to for custom syntax.

I agree with some of Tomas's points. DSLs are great when done right, but they can easily be overdone to the point of zero readability. On the completion note, I think it would be very cool if we had completion for some forms of custom syntax. E.g. if the parser optionally expects a keyword, that could show up as a possible completion. I imagine it would get complicated and heuristic-y very quickly, but it might be better than nothing.

[Sebastian Ullrich]

That sounds more like structural editing - suggesting just the next valid keywords is not terribly helpful I think, you really want to see the full alternatives in the grammar at this point, including alternatives that do not expect any further tokens. And there are some interesting modern implementation of structural editing that make it look actually practical, e.g. https://twitter.com/disconcision/status/1545085997972692992. But probably not something we should invest time on for Lean anytime soon...

3 years later: @dm_0ney and I, finally staring down the barrel of a multilingual structured editor with character-for-character text entry https://twitter.com/disconcision/status/1143367568796921858 https://twitter.com/disconcision/status/1545085997972692992/video/1

- andrew🦆blinn (@disconcision)

[Andrés Goens]

Mario Carneiro said:

This is a... complicated question, and the simple answer is that if you want a fully proof preserving shallow translation then no it's not possible in either direction. That post has to turn off a lot of coq kernel checks (including some that are critical for soundness) to make the proofs go through

Are you talking about just Gallina here or also Vernacular + Ltac(/2)? I could imagine that a decent subset of Gallina could be directly translated into Lean (leaving out stuff like coinduction)

[Andrés Goens]

I think it's different if you want to use libraries like Iris and you actually want to build something using them as a library, or if you "just" want the proofs of some statements to build op on them

[Mac]

Tomas Skrivan said:

Quite ofthen when I run go-to on some custom syntax it takes me to some code about generic elaboration in the main Lean codebase.

In my testing, all go-tos on Lake syntax take me to the Lake codebase (a decent amount of syntax also has docstrings). If it doesn't, that feels like a bug. I know that I often have the mentioned problem with builtin Lean syntax, but that is because the syntax is builitin and extra work has to be done to add the proper go-to location to the syntax (which was often not done -- its has gotten better with new release, though, in some cases).

[Mario Carneiro]

Andrés Goens said:

Are you talking about just Gallina here or also Vernacular + Ltac(/2)? I could imagine that a decent subset of Gallina could be directly translated into Lean (leaving out stuff like coinduction)

I was talking about Gallina, not tactics. The later comment about source-to-source translation was about tactics. It is true that a decent subset of Gallina can be translated, but a decent subset is not good enough to make whole files typecheck because you have to worry about the entire library that lead to them being in the subset, and that's almost certainly not going to be the case

[Yuri de Wit]

Tomas Skrivan said:

• lack of libraries: this is a problem for any starting language

Indeed and it is a chicken and egg problem. One way to mitigate this would be to make it quite easy to reuse libraries/packages from other, more mature and widespread languages. For example, it would be great to be able to add a cargo dependency to a Lean/lake project.

• overselling verification: people already interested in verification are already using Lean, Coq, Agda, ... They are small in number and just need to be convinced to switch to Lean. In my opinion, Lean is wonderful language even if you are not interested in proofs.

I know close to nothing about verification, but coming from the programming side, I see value in being able to program in Lean and iteratively prove more and more properties about it. It would be even better if this collaboration could span multiple people/teams (different expertises).

• custom syntax: I love the extensibility of Lean's syntax. However, I can see how every library creator will go nuts, define their own DSL, and using Lean will effectively requite learning dozens of poorly documented languages.

Yes, I share the concern. However, if Lean can make sure that all the capabilities available to core language features (syntax highlighting, go-to-definitions, hovers, doc strings) are also available out of the box for custom DSLs, this could become a real differentiation. Maybe it is already so to a great extent?

In fact, I find Racket's lead a good example on how Lean could fine tune features to make it a better 'language of languages'. My guess is that this is/was already in the devs mind since I even found (unused) #lang (a mechanism that Racket uses to better isolate and control the zoo of languages available) parsing code in one of the .cpp source files :-)

[James Gallicchio]

Tomas Skrivan said:

• overselling verification: people already interested in verification are already using Lean, Coq, Agda, ... They are small in number and just need to be convinced to switch to Lean. In my opinion, Lean is wonderful language even if you are not interested in proofs.

As someone with a more software background, I like Lean because I can express invariants in my code, especially if I can't prove them yet.

It's nice to never write a comment like (* NOTE: Requires some complicated condition on the inputs to behave correctly *) and instead to just write the condition as a hypothesis. Huge advantage IMO over other functional languages, even if you aren't interested in proofs.

(I guess there are also lots of people that aren't even interested in correctness, let alone proofs, but I don't think that's the target audience anyways...)

[Tomas Skrivan]

Mac said:

In my testing, all go-tos on Lake syntax take me to the Lake codebase ...

It was most likely a learned helplessness from my experience with custom syntax elsewhere.

I just want to mention that what I described was in no way a critique of Lake. It is more of an example what someone inexperienced might struggle with when dealing with custom syntax.