coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] [Agda] Why dependent type theory?

From: Gabriel Scherer <gabriel.scherer AT gmail.com>
To: Martin Escardo <m.escardo AT cs.bham.ac.uk>
Cc: James McKinna <james.mckinna AT ed.ac.uk>, coq-club <coq-club AT inria.fr>, agda-list <agda AT lists.chalmers.se>, lean-user <lean-user AT googlegroups.com>
Subject: Re: [Coq-Club] [Agda] Why dependent type theory?
Date: Mon, 9 Mar 2020 07:34:23 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=gabriel.scherer AT gmail.com; spf=Pass smtp.mailfrom=gabriel.scherer AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt1-f172.google.com
Ironport-phdr: 9a23:mpHirBVykgXb5zxZ4JqSpYF/41bV8LGtZVwlr6E/grcLSJyIuqrYbBWPt8tkgFKBZ4jH8fUM07OQ7/m8HzVZvt3Q7jgrS99laVwssY0uhQsuAcqIWwXQDcXBSGgEJvlET0Jv5HqhMEJYS47UblzWpWCuv3ZJQk2sfQV6Kf7oFYHMks+5y/69+4HJYwVPmTGxfa5+IA+5oAnMucQam5ZuJrszxxfGpnZFevldyH91K16Ugxvz6cC88YJ5/S9Nofwh7clAUav7f6Q8U7NVCSktPn426sP2qxTNVBOD6XQAXGoYlBpIGBXF4wrhXpjtqCv6t/Fy1zecMMbrUL07QzWi76NsSB/1lCcKMiMy/W/LhsBsiq9QvQmsrAJjzYHKfI6VNeJ+fqLDctMcWWpBRdtaWyhYDo+hc4cDE+8NMOBFpIf/ulQOtwOzCgaiBOztyjFGiHz407Ak3es9CgzJxhAsEsgUvXjIsNn4NqEfWv21wqnSyjXDautb1zbn54fTaBAhoO+DXbZtesTM1UYvFx3Kjk+Opoz/IjiY0esNvHKA4Op6VOKglWonpxtqojezxscjlJPJiZwPyl3f+iV5xZw6Jdy8SEJhfdGkF55QujicOoBrQc0iW3lltDgmxrACo5K2fygHxI46yxPed/CLaZWE7xD9WOuXPDx2nmhqeKiliBa36UWgyvPzVs2z0FtSqypKiNjMtnQU2xzK9siLV+Jx/km81TuNyQzf8O5EIUczlarUL54u3KQ8mYYUsUTGBiP2mUP2g7GKdkg85OSk9+Dqbq/lq5KcLYN4lwDzPrg0lsCiA+k0LBACX22B9uS90L3j81f5QLJPjvAunanWqovVJd4apqGnBw9ZyJ0j5Aq/Dzi4ytQXg2MHIUlKeBKClYfpOlXOLOrkAve4hlSgiC1ryOzePr39HpXNKWDOn6vmfbZk8kJT1A4zzc1E6J9PEbEAIPfzWlfru9DCDx85NRa0w+f9B9ln2IMeQzHHPqjMFarIrV6Ors80KOCWaIhd7DO7JuMu7uTiilcyghkXfaCsm5IcLm27SKdIOUKcNFXliM0AHGNChQE+QfbnkhXWXjdZfXe/W+Qn7TE2Eo+8JYjGT4GpxreG2XHoTdVtemlaBwXUQj/TfIKeVqJJMXrKe54zonk/TbGkDrQZ+1SrvQ7+xaBgK7ONqCIdvJPnktNy4r+KzExgxXlPF82Yllq1YSR0k2cPHWFk2al+pQlk1g7G3/En2bpXEttc4/4PWQA/Z8aFk75KTuvqUweERe+nDU68S4z/Uz40R9M1hdQJZhQlFg==

In this nice quote, foundations are considered from the perspective of expressive power:

What if we find mathematics that *cannot* be formalized with our choice of foundations?

In our experience with proof assistants, the discussion is generally not about expressive power (the possibility to formalize something at all) but about convenience, which in practice determines feasability:

What if we find mathematics that cannot be formalized *in practice* by our proof assistant, due to our choice of foundations?

It is not obvious to me whether this impact of foundations on practical usability of proof assistants is going to stay, or whether it is a problem of youth that will go away as we develop better assistants. I would rather hope the latter: that we can build proof assistants that are flexible enough to conveniently support a very broad range of mathematics.

Re: [Coq-Club] Why dependent type theory?, (continued)
- Re: [Coq-Club] Why dependent type theory?, Talia Ringer, 03/05/2020
- Re: [Coq-Club] Why dependent type theory?, Josef Urban, 03/05/2020
- Re: [Coq-Club] [Agda] Why dependent type theory?, James McKinna, 03/06/2020
  - Re: [Coq-Club] [Agda] Why dependent type theory?, Martin Escardo, 03/06/2020
    - Re: [Coq-Club] [Agda] Why dependent type theory?, Martin Escardo, 03/06/2020
      - Re: [Coq-Club] [Agda] Why dependent type theory?, James McKinna, 03/08/2020
        
        Re: [Coq-Club] [Agda] Why dependent type theory?, Martin Escardo, 03/09/2020
        
        Re: [Coq-Club] [Agda] Why dependent type theory?, Gabriel Scherer, 03/09/2020
        
        Re: [Coq-Club] [Agda] Why dependent type theory?, Jeremy Avigad, 03/10/2020
        Re: [Coq-Club] [Agda] Why dependent type theory?, Jeremy Avigad, 03/16/2020
        
        [Coq-Club] Type Theory vs. Set Theory – Re: [Agda] Why dependent type theory?, Ken Kubota, 03/09/2020
        
        Re: [Coq-Club] [Agda] Type Theory vs. Set Theory – Re: Why dependent type theory?, Thorsten Altenkirch, 03/10/2020
        [Coq-Club] Concepts within Type Theory – Re: [Agda] Type Theory vs. Set Theory – Re: Why dependent type theory?, Ken Kubota, 03/13/2020
        Re: [Coq-Club] Concepts within Type Theory – Re: [Agda] Type Theory vs. Set Theory – Re: Why dependent type theory?, Thorsten Altenkirch, 03/13/2020
        Re: [Coq-Club] Concepts within Type Theory – Re: [Agda] Type Theory vs. Set Theory – Re: Why dependent type theory?, Ken Kubota, 03/14/2020
        
        Re: [Coq-Club] [Agda] Concepts within Type Theory – Re: Type Theory vs. Set Theory – Re: Why dependent type theory?, Martin Escardo, 03/13/2020
        Re: [Coq-Club] [Agda] Concepts within Type Theory – Re: Type Theory vs. Set Theory – Re: Why dependent type theory?, Thorsten Altenkirch, 03/13/2020