Zulip Chat Archive

Stream: new members

Topic: comparisons


view this post on Zulip Wrenna Robson (Aug 20 2020 at 15:35):

I was wondering (currently working through Lean tutorial exercises) - what are the advantages/disadvantages of Lean compared to other proof assistants? What can't it do/what isn't it good for/what are its limits? I am really enjoying exploring it so far, but I'm wondering what the roof of the sky is, you know?

view this post on Zulip Patrick Massot (Aug 20 2020 at 15:45):

There are a couple of pointers at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/CICM.202020/near/206476084. But discussing this is not so fertile. You can simply try a couple of proof assistants. If you don't know where to start in order to learn Coq then you probably want to use Lean...

view this post on Zulip Wrenna Robson (Aug 20 2020 at 15:48):

That's fair enough!

view this post on Zulip Wrenna Robson (Aug 20 2020 at 15:52):

I suppose what I was trying to get my head round was why a project that already exists and uses Coq might use Coq in specific, say, but I suppose to a degree the answer is "time exists and we live now and not then", which isn't particularly fertile.

view this post on Zulip Patrick Massot (Aug 20 2020 at 15:58):

There is a lot of inertia here. Learning how to use a proof assistant is extremely time-consuming, and changing is difficult. Building a good library is also extremely time-consuming and discourages switches. There are also huge cultural differences that totally prevents many movements between communities. The Coq community has a huge bias towards constructive mathematics while most people here do regular mathematics. This is not a difference between software, but between people and libraries.

view this post on Zulip Wrenna Robson (Aug 20 2020 at 16:33):

That makes sense. I'm coming at it from a cryptography perspective and wondering if I might be able to get any use from it. Well: let me be more exact. I'm wonder if I could extract some useful research by writing some provable security stuff in Lean. Somebody has to be the first...

view this post on Zulip Wrenna Robson (Aug 20 2020 at 16:33):

It's fun regardless!

view this post on Zulip Frédéric Dupuis (Aug 20 2020 at 16:46):

You might also want to check out EasyCrypt (https://www.easycrypt.info/trac/), which is a specialized verification tool for cryptographic protocols.

view this post on Zulip Wrenna Robson (Aug 20 2020 at 16:47):

Nice, thank you.


Last updated: May 12 2021 at 23:13 UTC