Zulip Chat Archive

We're hoping that we can to translate all of the work and knowledge that has gone into Lean 3 code into Lean 4 code, when the latter comes out. So, you could start working with Lean 3 now with that in mind. Otherwise, you may have to wait for an indeterminate time.

Simon Hudon (Jun 27 2018 at 13:59):

I think it's safe to say that Lean 4 will be based on dependent type theory and make a similar use of functions and type classes so those are certainly worth knowing about even if their syntax changes

HT (Jun 27 2018 at 14:03):

@Simon Hudon It's the most clean and flexble one. It has best chance to unify programming and math.

Simon Hudon (Jun 27 2018 at 14:06):

To be fair, this unification is already happening. Coq has taken us a long way and so has Isabelle. Chances are that Lean will be another stepping stone in that lengthy process

HT (Jun 27 2018 at 14:16):

Those two looks like lots of math proving steps, it don't make sense to me. Lean and Fstar looks more like functional programming.

Patrick Massot (Jun 27 2018 at 14:17):

Lean looks like math much more than Coq (simply thanks to unicode use and less esoteric notations)

Sean Leather (Jun 27 2018 at 14:18):

In Lean, using tactics is, as in Coq, like proving steps in math.

Reid Barton (Jun 27 2018 at 14:18):

My impression is that people don't really use term mode in Coq, is that right?

Sean Leather (Jun 27 2018 at 14:20):

I've never seen it in any Coq tutorial.

Simon Hudon (Jun 27 2018 at 14:20):

My impression is that people don't really use term mode in Coq, is that right?

It's also my impression. The syntax of term mode is not geared for writing proofs

HT (Jun 27 2018 at 14:26):

@Patrick Massot Lean also looks like programming more than Coq at the same time.

HT (Jun 27 2018 at 14:41):

On the other hand, Coq makes no sense to low level programming. Lean has potential to prevent flaming chips and overflows.

Simon Hudon (Jun 27 2018 at 14:43):

Why do you say that Coq makes no sense to low level programming?

Reid Barton (Jun 27 2018 at 14:45):

My impression is that people don't really use term mode in Coq, is that right?

It's also my impression. The syntax of term mode is not geared for writing proofs

Oh I see, I had a hidden assumption in my mind "for doing math".

HT (Jun 27 2018 at 14:49):

Coq don't generates C which POSIX is defined by, and had a huge irreducible runtime with gc that could fulfill memory.

Simon Hudon (Jun 27 2018 at 14:50):

@Reid Barton I don't understand what your addition changes

Simon Hudon (Jun 27 2018 at 14:52):

@HT Coq has most of the major low-level verification frameworks that I know of. I don't know if they prefer parsing C or generating C but a lot of low-level verification is done with Coq. See Iris, Bedrock and VST

HT (Jun 27 2018 at 14:59):

@Simon Hudon They actually make developers less productive because of extra barriers. At least four languages involved in, EDSL to generate C , C, Coq, OCaml.

Reid Barton (Jun 27 2018 at 15:00):

I assume people do use term mode for programming (e.g., for program extraction)?

HT (Jun 27 2018 at 15:01):

When bugs wasn't catched by types, debugging must includes huge runtime with gc, edsl, coq, ocaml.

Simon Hudon (Jun 27 2018 at 15:03):

If I understand you correctly, what your getting at is better tools. It's not about low-level programming. It's about being productive as programmers

HT (Jun 27 2018 at 15:05):

@Simon Hudon Yes, Coq costs too much. I'm not sure why it's not about low-level programming, high level programming seldom encounters problems caused by runtime.

Simon Hudon (Jun 27 2018 at 15:13):

Your initial statement was "[it] doesn't make sense to low level programming". Is that still what you're arguing? If so, I argue that the frameworks I mentioned help understand low level programming.

Simon Hudon (Jun 27 2018 at 15:15):

Or maybe I should understand your point as being "it is difficult to use in low-level settings because of its awkward tools". In that case, I should agree. I haven't tried the frameworks in that context but it is consistent with my (small) experience with Coq

HT (Jun 27 2018 at 15:19):

To be more clear, I mean it doesn't make sense for programmers to cost so much barriers to correct code.

Simon Hudon (Jun 27 2018 at 15:25):

To be honest, that does not clarify your statement for me. It sounds like you're saying that a heavy run-time is one too many hurdles towards obtaining correct code.

HT (Jun 27 2018 at 15:27):

That's one point. And the other is there's too many concepts compounded in a inconsistent way.

Simon Hudon (Jun 27 2018 at 15:28):

Do you have an example to illustrate that point?

HT (Jun 27 2018 at 15:39):

I got an example. https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/theories/program_logic/hoare.v

HT (Jun 27 2018 at 15:40):

Why do we need hoare logic if everything could be proved in dependent type?

HT (Jun 27 2018 at 15:44):

I can not imagine I can convince any low level programmers costs so much time to learn several different theories nested in dependent types and three kinds of syntax, ocaml, coq, edsl, to start programming correct code.

Simon Hudon (Jun 27 2018 at 15:45):

Those are separate things. Hoare logic is formulated in dependent types. And dependent types by themselves are not sufficient, you need program semantics and verification rules. Particularly in the case of low-level code, the most effective tool around is separation logic which is formulated as a Hoare logic. The whole thing is still couched on a dependent type theory. The same way you wouldn't use a programming language without libraries, you can't use a logic without a certain number of basic theory

Simon Hudon (Jun 27 2018 at 15:46):

If you have something better than separation logic for low-level pointer reasoning, you should publish it. It's going to be worth a lot

Simon Hudon (Jun 27 2018 at 15:54):

As for convincing people, it doesn't have to be all or nothing, there are middle grounds, gateway drugs if you want, where very little effort yields a great benefit. TLA+ for example is tremendous if you want to learn formal specifications and use them in a project. With its model checker, you get a great benefit from any degree of formalization that you care to go through. In some cases, that can be enough. In others, you want a full functional proof of correctness. Then you have to invest time. Lean is not going to be a magic bullet any more than Coq is. With a wider community in the industry and in academia using formal proof, with can decrease the burden of writing formal proofs for sure but it's an ongoing process. Most importantly, it happens with people trying the tools, finding them lacking and adding their two cents

Patrick Massot (Jun 27 2018 at 15:54):

I have good news for the Lean 4 timeline. It seems Sebastian will not waste time watching his country playing in the world cup.

HT (Jun 27 2018 at 15:55):

@Simon Hudon I may be wrong, I though linear type reduce the use of pointers like rust does. We just need to seperate different kind of resources in types.

Patrick Massot (Jun 27 2018 at 15:57):

Brazil is still in though.

Simon Hudon (Jun 27 2018 at 15:59):

That's true and linear types are one of the tools that I'm mentioning. But the operating word here is "reduce". Reducing the use of separation logic is a great achievement. But with Iris project, we see that as long as you use unsafe code in libraries, you will need to use a least a little bit of separation logic to verify them.

Sebastian Ullrich (Jun 27 2018 at 16:00):

@Patrick Massot Today's events did not change anything in that regard :P

HT (Jun 27 2018 at 16:20):

I hope my point is clear, to write code fast and correct. Lean looks so handy to make most of the logic proved without much barriers. If I still needs something not covered by types, I'd write tests rather than involving additional layers of theories.

Simon Hudon (Jun 27 2018 at 16:23):

I agree in parts with your point. Lean and its tools are looking more and more like an IDE. You can use them to write programs without proofs, you can import various packages with varying levels of verification. You can be deterred by adding new logics to your system but making them available means that, when you decide that they're worth it, you can just reach for them.

HT (Jun 27 2018 at 16:31):

@Simon Hudon Yes, that's what I expect, a programming language.

Simon Hudon (Jun 27 2018 at 16:32):

Glad we found a common ground. I think compared to Idris (which might also fit your criteria), Lean is a better prover

HT (Jun 27 2018 at 16:36):

I also think Lean is better in a consistent way. I feel something wrong with Idris but I'm not sure what it is.

HT (Jun 27 2018 at 16:48):

It makes me feel that Idris is a variant of Haskell injected with extra type ability inconsistently which actually causes bugs rather than an actual type theory like Lean.

Sean Leather (Jun 28 2018 at 07:48):

I previously wrote:

We're hoping that we can to translate all of the work and knowledge that has gone into Lean 3 code into Lean 4 code, when the latter comes out. So, you could start working with Lean 3 now with that in mind. Otherwise, you may have to wait for an indeterminate time.

Simon responded:

I think it's safe to say that Lean 4 will be based on dependent type theory and make a similar use of functions and type classes so those are certainly worth knowing about even if their syntax changes

I agree with Simon, but I think there's a big difference between translating knowledge of basic concepts into an implementation (of which there are many: Coq, Agda, and Idris to name some popular ones) and translating an existing codebase and deep knowledge of one language into another.

The only public document reflecting the Lean 4 plan (at least for when it was written) states:

Users should not expect Lean 4 will be backward compatible with Lean 3.

This is why I conservatively referred to “hope.” I think there is some risk of working in Lean 3 now if you wish to move to Lean 4 later. But I also think there is some confidence that Lean 4 will not be as radically different from Lean 3 as, say, Coq is from any version of Lean.

Mario Carneiro (Jun 28 2018 at 07:52):

I think considerably more than Simon's list of concepts will carry over to lean 4. I know that "the syntax will stay more or less the same" modulo some easy regex fixes, but the elaborator may also change (semi by accident, because it will be re-implemented in lean), and this may cause more subtle breakage

Last updated: Dec 20 2023 at 11:08 UTC