Self-studying Lean4 with Software Foundations?

Stream: new members

[Trond Linjordet]

Hello,

Is this a good idea: taking the online book series and associated video lectures "Software Foundations" for Coq and trying to do the equivalent in Lean4?

[Henrik Böving]

If you are starting out with Lean I would suggest to use a Lean 4 resource to avoid learning 2 things at once. If you are particularly interested in software verification consider checking out https://lean-forward.github.io/hitchhikers-guide/2024/

[Trond Linjordet]

Thanks! Besides inconvenience and inefficiency of dealing with Lean and Coq side by side, are there major differences in underlying assumptions about software verification with Lean versus Coq?

[Henrik Böving]

If you are interested in specific niches it might be that the Coq eco system already has libraries that Lean doesn't but for all of the basic stuff not really.

[Kevin Buzzard]

FWIW my first lean project when I was an absolute beginner was working through the first half of the first volume of software foundations and translating all the exercises into lean. However this was back in the day where there were essentially no resources for learning lean other than #tpil which I also worked through. I then started trying to do undergraduate level mathematics.

[Trond Linjordet]

Ah yes, I probably heard about that from a podcast interview and it stuck with me.

[Trond Linjordet]

Thanks for replies!

[Kevin Buzzard]

I remember doing several exercises about various statements of logic several of which had names (eg Pierce's law) and all of which were to be proved to be equivalent to LEM and I think this was what inspired me to give up with software foundations!

[Kevin Buzzard]

It was this sort of experience which really hammered home to me the fact that there seemed to be very little documentation available at that time which was suitable for a classical mathematician, in any system

[Ilmārs Cīrulis]

Henrik Böving said:

If you are interested in specific niches it might be that the Coq eco system already has libraries that Lean doesn't but for all of the basic stuff not really.

Volume 5 or "Verifiable C" from "Software Foundations", probably, is related to this.

Volume 1 or "Logical Foundations" definitely could be skipped if one isn't interested in Coq/Rocq, and Lean books used instead.

Volume 3 or "Verified Functional Algorithms", hmm... is the https://lean-lang.org/functional_programming_in_lean something similar? I took a look at both and it seems that Volume 3 would be interesting to translate into Lean.

Volume 4 or "QuickChick: Property-Based Testing in Coq" --- not sure, but isn't Plausible (which I have seen mentioned here) something similar? Anyway, I have read nothing of this book, so no idea.

Volume 2 or "Programming Language Foundations" and Volume 6 or "Separation Logic Foundations" could be interesting to Program verification channel. And to me too, when I finish that "Concrete Semantics" book (which uses Isabelle/HOL, but I do exercises in Lean).

[Ilmārs Cīrulis]

Anyway, sorry, these are my 2 cents.

I have tinkered with Coq (now Rocq) for many years, before I started to use Lean/Mathlib for basic math things. I have fond memories of it. :sweat_smile:

[Ilmārs Cīrulis]

And thank you for mentioning "The Hitchhiker's Guide to Logical Verification" book. I didn't know about it. :)