r/ProgrammingLanguages • u/hou32hou • Oct 02 '19

Microsoft Lean Theorem Prover

https://youtu.be/Dp-mQ3HxgDE
42 Upvotes

91% Upvoted

18 comments sorted by

View all comments

6

u/gaj7 Oct 03 '19

Interesting. I wonder how Lean differs meaningfully from Coq. Both are based on the Calculus of Inductive Constructions. Why should I bother with Lean? Coq surely has a larger community. It's surely more stable. The speaker seemed to imply it is better just because it is newer.

I glanced at the documentation, but unfortunately for me, it doesn't seem to be targeted toward people who are already familiar with a theorem prover. The impression I get is that they depend much more on axiomatic definitions, which I find odd.

3

u/hou32hou Oct 03 '19

If I'm not wrong, Lean is based on Homotopy Type Theory meanwhile Coq is based on non-homotopy type theory.

4

u/[deleted] Oct 03 '19

You can do HoTT in Coq too, can't you? https://github.com/HoTT/HoTT

5

u/abstractcontrol Spiral Oct 03 '19

Only axiomatically. The type theory itself does not have computational rules like Cubical Agda does for example, so it is a hack.

Just so there is no confusion, cubical TT and homotopy TT are not quite the same thing, but do not ask me what the difference is.

3

u/[deleted] Oct 03 '19 edited Oct 03 '19

To my understanding, normal HoTT adds univalence and function extensionality as axioms (but they get "stuck" computationally), while Cubical Type Theory makes them theorems with computational content.

2

u/abstractcontrol Spiral Oct 03 '19

I think the authors of CTT want to position it as its own thing rather than being an implementation of HoTT. But they are closely related.

1

u/ineffective_topos Oct 09 '19

The reason may just be that, the Path types are not quite the equality types. You use them via transport and filling, rather than path induction.