Why use propositions as types?

Stream: Lean for the curious mathematician 2020

[Robin Allison]

This isn't a question about lean per se, but given that lean is based on CiC, I thought people in this community might be able to answer a question I've had for a while: What is the importance of the curry-howard isomorphism / propositions as types representation mechanism for formal proof verification?

There are plenty of proof assistants that don't follow this paradigm so that makes me ask why follow this unusual formalism (for most mathematicians) at all? I mean, it must have some very compelling advantages and I wonder what those are.

The term that immediately comes to mind to explain its advantages is "computational content". Formalisms based on the lambda calculus have computational content because terms of the lambda calculus are programs and "run" through beta reduction. I don't see how this benefits formalization at all. How can a computer use this to verify a proof is correct? It is easy to conceive of some program that can run through the steps of a proof and verify it is all correct. I can't conceive of proofs themselves being programs as somehow helping this process. The only thing remotely relevant in my mind would be how a lambda term denoting
an arithmetic expression, e.g. (2+2)*3, can be evaluated to an integer by running the program it is encoded as.

Now evidently I don't entirely understand what this term means as people will say, dependent types for instance have a computational interpretation, and a big problems apparently is how adding axioms to these systems, for instance function extensionality or the univalence axiom, may not have a computational interpretation. My understanding at the present goes that each term describes an algorithm for constructing a term of a given type. The function type operator is a primitive constructor or algorithm for constructing a terms of one type out of a term of another type. But what is to stop you from asserting other axioms have a computational interpretation?

For example function extensionality would be a term of the type
(A)(B)(f:A\toB)(g:A\toB)((x:A)(f(x)=g(x))\to(f=g)).
(apologies for the awful notation) What is to stop us from regarding this as a primitive construction? In terms of classical logic this is like adding an extra axiom and I would ask "is this consistent", but I'm not sure what the right question to ask here would be. It must be the case that the formal system has certain properties or not whereby we deem such an axiom to have computational content or not. Such formal properties may suggest what advantages "computational content" confers upon a proof assistant but I don't even know what these properties would be at this point. (canonicity property?... and how is it even possible to have a closed term of type int that doesn't evaluate to a numeral?)

Along these lines is the decidability of type checking. This is important because type checking corresponds to proof checking. As I understand it type checking is decidable if we have an algorithm to determine if a term in a given context is of a given type, but isn't this redundant in a proof assistant where the entire point is to interactively construct a term of a given type. You wouldn't need to check a term is of a given type because your construction is already an algorithm to verify this.

The second possible line of advantages in my mind is that type theory just more closely reflects how most mathematicians think. Cue remarks on synthetic euclidean geometry and nonsense terms you can form in set theory such as the intersection of + with the number 9. I could regard this as a compelling reason for CiC, just not in isolation. So really I'm more curious on the computational angle here.

[Notification Bot]

This topic was moved by Bryan Gin-ge Chen to #Type theory > Why use propositions as types?

[Bryan Gin-ge Chen]

Hi Robin, hope you don't mind, but I've moved your post to the #Type theory stream where it might be seen by more interested folks.