Zulip Chat Archive

Stream: new members

Topic: Henry Story


view this post on Zulip Henry Story (Sep 28 2020 at 06:19):

Hi, I am exploring the space of proof assistants and got pointed to Lean from the category theory zulip channel via a youtube presentation by Scott Morison. (That's all I now at present). It looks very nice.
The Lean Doc says

A prior version, Lean 2, had special support for homotopy type theory.

which of course raises the question if that has been integrated into Lean 3, or if that is a dead end project, or if something even better was planned (e.g. Modal HoTT)? I was just curious.

view this post on Zulip Scott Morrison (Sep 28 2020 at 06:50):

There is a project doing some HoTT in Lean3: https://github.com/gebner/hott3, but it is not particularly active.

view this post on Zulip Scott Morrison (Sep 28 2020 at 06:50):

It demonstrates that it is possible, but there doesn't appear to be much interest in pursuing it at the moment.

view this post on Zulip Henry Story (Sep 28 2020 at 06:51):

I had just found that, following a link from this page. :-)

view this post on Zulip Scott Morrison (Sep 28 2020 at 06:52):

Most of the community of mathematicians working with Lean are very happy to work in classical foundations (well, if "classical" includes dependent type theory), and are more interested in doing "mathematics" as usually practiced.

view this post on Zulip Scott Morrison (Sep 28 2020 at 06:52):

That said, for a mathematician to learn the basics of dependent type theory, the first few chapters of the HoTT book are great, even if you have no interested in univalence.

view this post on Zulip Henry Story (Sep 28 2020 at 06:55):

yes, I agree, the first few chapters of the HoTT book are great.
I am actually coming from programming background in Scala (Odersky pointed me to HoTT 6 years ago) and so I have made a detour through Category Theory.

view this post on Zulip Scott Morrison (Sep 28 2020 at 07:11):

I'm a mathematician, but my programming background is partially in scala. A bit of a strange language, but I do like it. Lean is better, though, and Lean4 will actually be a proper programming language (not just a proof assistant), so all the scala folks should come join us. :-)

view this post on Zulip Henry Story (Sep 28 2020 at 07:33):

Very cool! When will that come out?
Two key features would be compiling to JavaScript and I believe to Web Assembly (I have not used WAssembly yet - and know little of it - but as I understand it could allow one to write very efficient reasoners for the browser, something I am interested for the semantic web. My understanding is that Web Assembly can be thought of as a new type of bytecode. As I understand it also allows one to compile existing c programs to it).

view this post on Zulip Patrick Massot (Sep 28 2020 at 07:38):

Lean3 itself compiles to Wasm, this is what you see at https://leanprover-community.github.io/lean-web-editor/

view this post on Zulip Patrick Massot (Sep 28 2020 at 07:39):

(Lean 3 is a C++ program)

view this post on Zulip Patrick Massot (Sep 28 2020 at 07:39):

There is no release date for Lean 4, but the first alpha version seems pretty close.

view this post on Zulip Patrick Massot (Sep 28 2020 at 07:41):

And indeed the situation with HoTT is: many people here would love to see it usable, but it currently isn't, so we play with what works today. This is not proof assistant specific. There is no sizable library of general mathematics formalized in HoTT, in any proof assistant. General mathematics here means what you learn in an undergrad math degree. Existing HoTT-based libraries are all about category theory and even more about HoTT for its own sake.

view this post on Zulip Patrick Massot (Sep 28 2020 at 07:42):

About Wasm, don't expect your web browser to execute Lean at any speed comparable to the native speed of course.

view this post on Zulip Henry Story (Sep 28 2020 at 08:02):

It's very helpful to know that the browser version is running wasm. That's helping me see what wasm is capable of :-)
I am very interested in proofs mostly for security reasoning. That's also why I have been looking to Modal HoTT as security reasoning can be seen as a form of modal logic. See e.g. Martin Abadi's work (An MS fellow) such as Access Control in a Core Calculus of Dependency. That should be doable with CoC based tools as it only requires Indexed Strong Monads, but I like to know what I may be missing :smile: .

view this post on Zulip Scott Morrison (Sep 28 2020 at 08:47):

Modal logic per se doesn't need any HoTT, of course, and has various partial formalizations in standard proof assistants.

view this post on Zulip Henry Story (Sep 28 2020 at 08:54):

yes, David Corefield who wrote the (philosophically oriented) book Modal HoTT only gets to the latest HoTT work in the last chapter of the book. But his key point as I understand is that modalities arise out of adjunction of slice categories.
As I understand the Modal HoTT work is showing how all modalities such as linearity, ... can be brought under one roof. But it's over my head at present. I need to become fluent in proof assistants to get to understand that first :-)


Last updated: May 13 2021 at 22:15 UTC