Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Lamport on TLA+ in Quanta, with Coq mention

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Lamport on TLA+ in Quanta, with Coq mention


Chronological Thread 
  • From: Andrew Appel <appel AT princeton.edu>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Lamport on TLA+ in Quanta, with Coq mention
  • Date: Tue, 17 May 2022 14:10:03 -0400 (EDT)
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=appel AT princeton.edu; spf=Pass smtp.mailfrom=appel AT cs.princeton.edu; spf=Pass smtp.helo=postmaster AT violeteyes.cs.princeton.edu
  • Ironport-data: A9a23:flsH1aBGExj1kxVW/8jlw5YqxClBgxIJ4kV8jS/XYbTApGl23jcPy WceWGuAPqrYZzSge9gkYIW/9UoE7cfdzNEwOVdlrnsFo1Bi+ZOUX4zBRqvTF3rPdZObFBoPA +E2MISowBUcFyeEzvuVGuG96yE6j8lkf5KkYAL+EnkZqTRMFWFw0HqPp8Zj2tQy2YXgXFvX0 T/Pi5S31GGNi2Yc3l08sPrrRCNH5JwebxtF1rCWTakjUG72zxH5PrpHTU2CByeQrr1vIwKPb 72rIIdVUY/u10xF5tuNyt4Xe6CRK1LYFVDmZnF+A8BOjvXez8A/+v5TCRYSVatYoyqEnuJO0 IlMiYWPSlsCEY/8x6clXiANRkmSPYUekFPGCWa+tsie00DXfmCqyO4oFFs3O4YV5uFxR2xC6 JT0KhhUNEDF3rvshuvgFK8x26zPL+GzVG8bknh41TzdJf09B4jZQqPB6MNf2nE9it0m8fP2P pZCN2I+NUqojxtnN2dNOMpljLyUhEb0YRkHjnLWjpQw7D2GpOB2+OW9YYGNJ7RmX/59lUGB4 2nC4m7RGQAfLNXZyDyf83vqiPWnoM/gcJwTE7m16vN7jUbVzXdVEAcXU1C2vf6/zEOyRrqzN nD45AIxoKkAy1T3T+XkYB7ki1GmjkFfY9dpRrhSBB629oLY5AOQB24hRzFHacA7uMJeeQHGx mNljPu1XWcy6+X9pWa1s+jI827uYED5OEdYPUc5oR05D84PSW3ZpirVT9BoHbKyiLUZ8hmok 23W8EDSa501gNFD9aih5l3W6w9AS7DXTwkx6xnaT2++qAhiIpa/Zoqj5ETc67BNIJvxori9U Josx5n2AAMmVM/leMmxrAMlRuzBCxGtamK0vLKXN8N9nwlBAlb6FWyq3BlwJV1yLuEPciLzb UnYtGt5vcEOZiTwMP8tM9/tV6zGKJQM8/y5Cpg4ifISP/BMmPOvpkmCmGbJhD+xzxJEfV8XY 8zHGSpTMZrqIfk3nWHuGo/xIJcz3CE4zm7PQpaz0hKmz7eEf3+JWN843KimM4gEAFe/iFyNq b53apvboz0CAbKWX8Ui2dRMRbz8BSRkVMCeRg0+XrLrHzeK70l7UK+MneJ4ItE690mX/8+Rl kyAtoZj4AKXrRX6xc+iMxiPsZvjAsRyq2wVJyspMQr60nQve9/xvqwEMYMtfL8s+fBky7h5Q +RcI5eMBfFGSzLm/TUBbMSh8NA6Kkjz3Q/ebTC4ZDUffoJ7Q12b89DpSQLj6S0SA3flrsA5u bChilvWTMNbFQRvBcrbcty1yFa1sSRPke5+RRKTcMFJeUPn/ZRtLWr8guJue5MALhDKxz270 QeKAEpE+bWV/dNtqNSQ3PKKtYakFed6D3F2JWiD4ObkLzTe80qi3ZREDLSCcwfCWT6m466lf +hUka3xaaVVgFZQvoNgOL931qZitcD3rrpXwwk4TnXGa1OnVuFpLnWch5YdqKxKwrJFtBq7Q QSE4Z9CI7SPM875F1hXKQY4N7zR2fYRkzjUzPI0PESnuHMrpOTbCR1fb0uWlShQDLppK4d0k +4utfkf5xG7lhd3YM2NiTpZ9jjUI3FcAb8rsIoWXN3ihgYxkA4Qf53bDiLq7YCCcJNHKQ8yO D6Sj6fegLIay0bfKiJhGX/I1OtbpJIPpBEXkANefwrVwoLI1q0twRlc0TUrVQAEnBxI3tV6N nVvK0Aod76F+C1lhZQbUm2hc+2b6MZ1JqAlJ5o1eGzlo42ASG3KKGAhNPeA5wYS6CREZDld9 7yEz2CjXDr3FC009jVnQlZr8pQPUvQonjAuWuj+dyhGI3X+STH+xLe0ZGwDpgfgB4U8iFCvS SxC4rNrcaOiXcIPi/RTNmRZvIj8jDicPm1ESvx9+6VPEG3BEN13Nf5iNGjpEv5wyzf2HYNUx iCgyg+jl/hz6cpWkg0mOA==
  • Ironport-hdrordr: A9a23:jo29Wa5H0RcAWk5IvAPXwMvXdLJyesId70hD6qkRc202TiX2ra qTdZgguCMczQx+ZJhCo6HiBEDjexzhHPdOiOF7AV7hZmjbUQCTTL2KmLGSpQEIbBeOkdK1u5 0NT0EHMqyVMbEst7ee3DWF
  • Ironport-phdr: A9a23:Eg4DPxeDUxETTqQKfkWYg4jSlGM+FdTLVj580XLHo4xHfqnrxZn+J kuXvawr0AWSG9iEoKsd1KL/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQF cVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHNbQhEnjqwbLF9I BmrsAnctNQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2U bJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5 KptVRTmijoINyQh/W/ZisJ+kqFVrxCvpxJizIHbfICVOv1ifq7GZ9wWWXZOU9xLWiBdAI6xa ZYEAeobPeZfqonwv0cDrR2jCgm2GuzuxCJDi2Pu3a0izeshFRzN0Qs6ENIWqHTbstH1ObwKU eCvzanIyynMYO1K2Tf67ojEaA4uruyRXb9pd8fa1EYgGR/fgFqKtYzlIy2a1v4Ls2WD8+ZtU eaihmElpgx+rDWhyMchhIbHi48b113J6Tt1zYQ1K9O4SEN2ZdGpHZlUuiyUKod4TcMvTmFnt iokxLALupi2dzUExpQgwh7Qcf2Hc46Q7xL6SeaeOzF4hG5/d7K6nRmy/lKvy+z9VsmyzllGt C1FksPDtn0Lyhfd6dCHR+Ng8ku/2juDzR3f5vxaLUwuiKbWJZ8szqQwm5cTqUjPAzH6lUbsg KKVeUgo4PWk5/rnb7n8u5OQKZN4hhnjPqgwmcGzG/k0PhUQU2SB5Oix2rzu8Vf5TbhIiPA9j 7TXsIjAKsQepaC5Gxdb3Zg/6xexCDemytcYkGEaIF5bex+LlZXlN0zQLPziEPuyjVWhnC1ry v3GJrHtH4vBI3vZnLv8YLpx9VRQxBc9wN1e/Z5ZCrMMLfTuUUHrrtPYFAU2MwmszubnFtp90 oQeVHqRAq+YN6PStUGH5v4xLOiMeoAVoyzxJOQ+5/L0lX85g14dfa+10pQJdHC4GfJmL1+Hb nXxn9cNCWYKvgwgQ+z2kFCOTCBfanWoU64h+z03FpiqAZrNS42smrCM3Ce2EoVTZm9cC1CMF Xnod5+DW/cJcC+dONdhkiQaWrilUIIuyQquuBXiy7p9L+rU/DEXuoz/1Nhy4e3fjw89+iFpD 8iF1WGCVHl7nnkUSD8uwKB/vUt9x0+e3aRgmfxXCcRT5+9VUgc9LZPT0+t6C8nrVg3deteJV U2pT869ATAxS9Ix28UBb1x8G9WklBDD3jClD6Ubl7yRV9QI9ffX2GG0LMJgwT6S3644ylIiX 8FnNGu8h6c5+RKFVKDTlEDMvqCmb6kDlAfV7GqHhT6HpFlVVCZoS6TDVn0DYU2QoNjksBCRB 4SyAKgqZ1MSgfWJLbFHP4WBZTRuQf7iPI+beGetgyKrAg7OwLqQbY3scmFb3SPHCUFCnRpAt W2eO10YASGs63nbECQoDUjmNkr06eR6gGuhT0k/wh2NaQts26fmsgUNi6mkQugIlqkBpD9nr jx1GFin2NeDAsKYqg5Jd74aeck85lxKyWXf8QFxI8/oNLhs02YXaB8/pEbyz1N3B4FHxNAtt 28vxRFuJLiwzlJGcz6E0IH9IfvcMS/q5hGpYKPK3VeY3dqLkksWwNI/rVir/ASgF055tm5iz 8EQyHyEoJPDEAsVV5v1FEcx7Rlz4b/AMGE74MvP2HtgPLPR0HeK0s81BOYj1herfstOeKKCG gjoFsQGBs+oYOU0klmtZxgAMahc7qkxd8+hcvKH3uasMoMC1HqvlXxK5KhlyEOK/CdgTeiO0 poYgrmZ0gaBSzbgnQK5qMmk0YtAZDwUAi++0X29Xt4XP/QoO99QVyHzfp7SpJ02nZPmVn9G+ UT2AloH3JTsYh+Odxnm2hUW000LoHuhkC/+zjpukjhvoLDMuU6Gi+nkahcDPXZGAWd4ilK5a 4Gsl90edEOzKRAzlR2u6Fr9we5WqLk1fAyxCQ9YOjP7KW1vSP76v6Kabspn8Ikpty5aTOO6J 12WV/Su6wtf2CTlEWxEwTk9fDz/oZT1kStxj2eFJWpypn7UES1p7S/W/8eUBftY3z5dATJ9l SGSHV+ked+g4dSTkZ7H9OG4TWOoEJNJI2HnyoaJtS3z4mMPY1X3luirl9nPGhN8yTX60dJnS SLO6hvwf8Hn2r+7PuRuYkRzTAamu4wjQ9s4y9BuwsxNkXEBzo2Y538GjXv+PbA5kerlYXwBS CRKi9/Z7Q752VFye3eAxob3THKYkYNqY9i3ZH9T2zpotpoaTv7NtvodxnUz/wfryGCZKeJwl Toc1/Y0vXsTguVS/REo0j3YGbcKW09RIS3rkR2MqdG4tqReImi1It3SnAJzm86sCLaar0RSQ nH8L90rBTd96u10KxTUynz14Yz4f9+WYN4O/E7x8V+In61OJZQ9m+BfzyN/IW/5lXY+jfYhj Bpl0I29us6KJ3gnr8fbSlZIczbyYc0U4DTki61Ty92X046YFZJkAjwXXZHsQKHgAHcIuP/gL QrLDCwkpyLRB+/EBQHGohQDzTqHA9WxOnqQPnVc0dhyWEzXOhlEmA5NFDAq1p8hSlLznpynK R4joGlKuBig7UEXr4Agfxj5WWPCqAr6ci01TpOSMB1QqAxO+g/DOMiapIqfBglg94a65EyII 22fPEFTCH0RH1eDHxblN6Wv4t/J966ZAPC/Jr3Ae+fGpetbXvaOjZWht+kuty6LLdmKN2J+A ucTxEtEWX1lFtXUgHMEUGoPjSPLZMOHoxH69yFq5syy6/XkXgvz6JDqafMaaI8/vUnv2+Hab LDW2XsxIC0Qzp4WwH7U1LUTlEUfjS1jbXjlELgNszLMULOFmqJTCE1+CWs7P89J4qQgmwhVb JeB2pWsj+Q+16VrTQoYBjmD0omzaMcHIn+wLgbCDUePb/GdICHThtrweeW6QKFRi+Nds1uxv yyaGgntJGfm9XGhWhaxPOVLlCzeMgZZvdT3ew51BGzLR8mgcge6NtR6kTowh7A4mzmZUAxUe Sg5aE5LorCKuGlAhe5jHmVa8nd/BfeFnCKU8+TJJ41QuuAtGj51kelX/HM8jbZZ8WsXIZ490 DuXpdlorVa8l+CJwTcySxtCpAFAg4eTtFljM6HUpdFQHGzJ9xUX4SCMGgwH8pF7X8b3tfkam b2t3OrjbS1P+NXO8Y4ACtjIfYiZZWE5P0OhEXaRBQ8BB1ZD2knUnApFivCU/XCJqZ58p5Txy sNmolpzTEY0EPgXFkNjWtEOPcUvNtvFuaCai8oF+XevoQKXT94cporGUPmfHfLpbjuVkOsdD yY=
  • Ironport-sdr: +75v8eED2GEN00QGQWrIJRBTBfvbcC32yGeMOy9eFArg0V0hdF7sI/NGu+H9XlmS+xP7tdO3kw p1H+i8AD/E1Fhw9atHIk7SqCFW9PMWLyCTjLkiWrQctBJn/FucMSGV/OGD/P8MQA9PhvMYs70S 9+0He7ZOfM9ABShyVBSdYJWfzNd9V2UN4tAGo4ugTOQc4zpdAdEAxk+WJrwTD4BQ/E60R9kKv0 6D2Y9md/7/LRBwhJskI3Y8EiLiyaSElnpdjNOzzzwcp9+ffeCd4ji0q6FzQ6IzJjQY+qi10pp4 CAa5hm5nNfycxHMHFA/lD4Mp

I'm not sure that Coq was designed to do real mathematics.

Perhaps its original designers intended just to demonstrate the Calculus of Constructions and to show a few things about proof assistants.
Perhaps they were as surprised when, after 20 years of development (1989-2009) by a talented team, plus 20 years of Moore's law increase in memory sizes and processor performance, it was shown that one could do real mathematics (and software verification) in Coq.  

Just speculating.   Perhaps some of the original Coq designers have opinions on this question.

-- Andrew Appel

From: jonikelee AT gmail.com
To: "coq-club" <coq-club AT inria.fr>
Sent: Tuesday, May 17, 2022 1:36:25 PM
Subject: [Coq-Club] Lamport on TLA+ in Quanta, with Coq mention
https://www.quantamagazine.org/computing-expert-says-programmers-need-more-math-20220517/

"Coq was designed to do real mathematics and to be able to capture the
reasoning that mathematicians do. ... TLA+ is designed not for
mathematicians but for engineers who want to prove the properties of
their systems. "

IDK.  I do however appreciate his emphasis on improving
"mathematical thinking" instruction for programmers.  But if you manage
to accomplish that, would they not then favor Coq over TLA+ as a
result?  Or, perhaps he is taking a pragmatic stance wrt education: it
won't change, programmers will continue to fear math, so TLA+ it is.



Archive powered by MHonArc 2.6.19+.

Top of Page