The Coq mailing list

[roux cody <cody.roux AT gmail.com>]

I'm only loosely associated with Lean, so I won't presume to speak for the motivations of all involved.

I think part of the motivation from the Z3 side was that for many applications, using tactic like hints was becoming a reality, which naturally leads to considering a full-fledged interactive theorem prover with powerful proof strategies. In addition, it's terrifyingly easy to make subtle soundness mistakes in SMT solvers. Backing one into an ITP from the start forces you to be honest.

Leo considered several languages for implementation, including Ocaml. While I'm certain his familiarity with C++ played a big part in the final decision, he has very justified reasons for choosing it. He claims that it's extremely hard to get excellent performance without breaking the nice abstractions built by such languages (memory management, data structure layout etc.), and I have to say, Lean is blindingly fast when type-checking. A lot of things become easy when working with such a mainstream language, like writing FFI bindings and using compiler frameworks.

As a social stepping stone, there is a type-checker for the kernel implemented entirely in Haskell, which is well-maintained at the moment I believe: https://github.com/leanprover/tc. It's pretty neat. The C++ code is also cleaner than I thought possible. Perhaps surprisingly, the C++ kernel is only about as large as the one in Coq I believe (though this might just be explained by it's relative youth).

The theoretical differences between Coq and Lean have been pretty well summarized. I think the practical differences are probably more important in the long run. The striking features are the web interface, the full concurrent type checking, and the excellent emacs-mode, which type-checks as you write and auto-completes in the eclipse style. The standard library is shaping to be very generic (based on type classes), and while smaller, is looking more like the MathComp library than the Coq standard library, so there is really an opportunity for a do-over here.

I believe Coq either has or is in the process of acquiring these features though, so it's still hard to say which are the real distinguishing things (though the Agda-style unicode bindings are just so fun!).

Jonathan sums it up the best I think. Lean is another point in the design space of dependent type based ITPs, with a lot of opportunities for trying out things that are impossible in Coq because of backward compatibility or just size and complexity.

Best,

Cody

This email has been sent from a virus-free computer protected by Avast.
www.avast.com

On Thu, Feb 25, 2016 at 8:54 AM, Bas Spitters <b.a.w.spitters AT gmail.com> wrote:

Yes, Jeremy's Isabelle background can be seen too. The proofs are,
arguably, more readable than Coq proofs.

The lean tutorial gives a good overview of the system.

On Thu, Feb 25, 2016 at 12:01 PM, Freek Wiedijk <freek AT cs.ru.nl> wrote:
> Hi Jonathan,
>
>>It looks eerily similar to Coq.
>
> I also is quite different from Coq in some respects.
>
> It is implemented in C++, not in ML.  It has proof
> irrelevance, function extensionality, classical logic, even
> a choice operator as part of the standard setup (exactly
> which of those are hardwired in, and which ones are just
> conventionally available in the library, I don't know.)
> It has been explicitly designed to be useful for HoTT (how
> that can be true in conjunction with the previous sentence, I
> don't know :-))  The type theory is simpler: they don't have
> "match" in the foundations, but instead work with recursors,
> and they don't have universe cumulativity.
>
> Jeremy Avigad is one of the people behind Lean.  He comes
> from an Isabelle background.  I can imagine Lean will feel
> more familiar to Isabelle people than Coq does.
>
> Freek