The Coq mailing list

[Mario Carneiro <di.gama AT gmail.com>]

On Tue, Jan 7, 2020 at 8:51 PM jonikelee AT gmail.com <jonikelee AT gmail.com> wrote:

[decloaking from lurker mode to add my $0.02]

Does having LEM built into Lean interfere with the user's ability to exploit the Curry-Howard isomorphism?

If so, that seems like a bad trade off: a small convenience for a
small group of people (Fields Medal wanabees) that imposes a large
inconvenience for a large group of people (software engineers).

I haven't found that Lean's ontology poses any serious issues for writing software, and if anything I think it helps. Lean makes a sharp distinction between data (in Type) and proofs (in Prop), and proofs are erased during code execution. So if you build a sorting function of type forall l : list A, { l2 : list A | l2 is a sorted permutation of l }, then the "list A" part is data, which can be executed assuming it doesn't use the axiom of choice in its definition, and the "l2 is a sorted permutation of l" part is a proof, so it completely disappears during execution. You can use choice if you want to prove this fact, as it is just a conventional mathematical assertion; it will not interfere with the computability of the overall function.

So it's a half-baked kind of constructivism, that is constructive only in the places where it actually matters to producing code. That seems like a reasonable compromise to me. In particular, LEM is not executable in any case, because it is a Prop; you can't case analyze on it unless you are proving another Prop and this too will be erased. Whenever you use "if" in Lean it infers decidability of the predicate in question, and this proof of decidability lives in Type and can be executed.

I could find no literature on Lean’s VM, and there is very little literature on Lean in general. This is a bad sign.

I could say a few things to respond to this.

(1) Lean comparatively young, and most of the academics who work on CIC as a type theory have been using Coq for a long time now, so unless they feel inclined to look at lean I don't see how this is going to just happen.

(2) I will point you to my paper https://github.com/digama0/lean-type-theory/releases/tag/v1.0 which tries to lay out the complete type theory that Lean implements, or at least an overestimate of it. There are many papers about subsets of Coq but I don't know any analogous paper that writes down everything the kernel is capable of doing, and I personally will not be convinced of the reasonableness of Coq as a formal foundation until this is done.

(3) The lean VM is a complicated compiler, and it is undergoing some significant changes in the newest version, but there is a reference for some of it: https://arxiv.org/pdf/1908.05647.pdf . Certainly it's not all you might like, but it at least satisfies an existence claim.

Mario