Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • From: "jonikelee AT gmail.com" <jonikelee AT gmail.com>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: [Coq-Club] Lamport on TLA+ in Quanta, with Coq mention
  • Date: Tue, 17 May 2022 13:36:25 -0400
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt1-f170.google.com
  • Ironport-data: A9a23:kOOg4K++Hg5+XMHhdgApDrUDvHiTJUtcMsCJ2f8bNWPcYEJGY0x3m zcdW2GAMveLMWbzc9ByPY238x9SucPTytYxSwtq/itEQiMRo6IpJ/zJdxaqZ3v6wu7rFR88s Z1GMrEsCOhuExcwcz/0auCJQUFUjP3OHvymYAL9EngZqTVMEU/Nsjo+3b9g6mJUqYLhWVnV5 Iqt+5e31GKNglaYDEpEs8pvlzs05JweiBtA1rDpTa0jUPf2zhH5PbpHTU2DByOQrrp8QoZWc 93+IISRpQs1yfuC5uSNyd4XemVSKlLb0JPnZnB+A8BOiTAazsA+PzpS2Pc0MS9qZzu1c99Zl uRmqN+BQiMVZvPIuMNBVR4HISciBPgTkFPHCSDXXc27ykTHdz7136wrAhhpZcsX/eF4BWwI/ vsdQNwPRkrb1qTmnfTiFLEq35t7RCXoFNt3VnVIzzbfDPUrRZ3Oa6rP7N5cmjw3g6iiGN6HO 5FEOWAzPHwsZTUQAmxLFZwenty6oUL0U2IbmmrPjoAOtj27IAtZieCxarI5YOeiTsJM202cu 2ju5HX8GhhcNdqFyDPD/GjEuwPUtSbyWYZXDaHhs/Az3wXVyWsUBxkbE1C8pJFVl3JSRfoBG mcJuRsliZRqqkiLaYX7WEKKpiK960t0t8VrL8U27wSEy6zx6gmfB3QZQjMpVDDAnJ9nLdDN/ g/Z9+4FFQCDo5XOFi3Arub8QSeafHlKfTVbNEfoWCNcu4G7yLzfmC4jWTqKLUJYptj8GDW12 izT6SZn2O1VgskM2KG2u1vAhlpAR6QlrCZlum07vUr/tGuVgbJJgaT2sTA3Ct4edO6koqGp5 iRspiRnxLlm4WuxvCKMWv4RO7qi+uyINjbR6XY2QcR7qG7wqyT9INEKiN2bGKuPGpZVEdMOS B+D0T69GLcOVJdXRfQqP9zoUJxCIVbITI29Day8giVyjmhZLVfbpkmClGaf2GfilEVErE3ME cbzTCpYNl5DUf4P5GPuGY81iOZ3rghjmz67bc2kl3yPjOvGDFbIGOxtGAbfPogRsvnYyC2Lq I03H5XRm31ivBjWOHa/HXg7dgBUcxDWxPne96RqSwJ0ClA9SDx9WqaInOxJlk4Mt/09q9okN 0qVAidwoGcTT1WeQelTQnw8Or7pQ7hlqnc3YX4lMVqyiiosZI+u6OEUcJ5uJesr8+lqzPhVS fgZepXYUq4fFGifozlNP4PgqIFCdQiwgV3cMiegZg85dcEySgHM/OjiYQaypjIFCTC6tJdlr rD5jlHbTJMPSh5MFsHTbP7znVq9sWJMyu13VkrMZNJUfRy0ooRtLiXwiN4xIt0NeU2TnGvEi 17ODE5B9+fXooIz/N3Yvoy+rt+kQ7lkA05XP2jH9rLpZyTX+2yUx4UfAuuFeDbqUnytpPeva OBT+PHLMPMdmWFMvYchQa1gyrgz5oe2qrJXklZkEXHMYwj5A79sOCPaj8xGt6kI36MA/AXvB RrJ9d5dNrGEfsjiFQdJdgYia+2C09ASmyXTvatpehSkvHcv8erVS1hWMjmNlDdZcOl/PrQjz Lpzo8UR8QG+1kcnP4rUlCxS7GjQfHUMX7996sMfCY7vzxM3kxRMOMOETCDx556LZpNHNUxze m2Yg6/LhrJ9wEvecipsSSKcg7IF3Zle6gpXyFIiJkiSnoaXjPEA2hAMoy88SR5Yz0ka3u9+U oSx25aZ+UlTE/ZUaMl/s6SEHghAAFiA5hW0xQJWzCvWSE6nUmGLJ2o4UQpIEIb17EoEFgW3P pnBoIombdouVM701yo2H0VirpQPiPRvoxbalpnP89utRvEHjPmMvkNqTWUNohrjR8g2gSUrY AWsEPlYMcXGCMLbn0H350R2G1jdpNBo6VGumc1cwZ4=
  • Ironport-hdrordr: A9a23:FlUTyqob6hwtrJ04KiiYNS0aV5oaeYIsimQD101hICG9Ffbo7P xG/c5rrSMc7Qx6ZJhOo6HiBEDtewK/yXcX2/hpAV7BZniAhILAFugLhuvfKlXbehEWndQtsZ uIHZIObeEYzmIXsS852mSF+hobr+VviJrY49s2Bk0CcT1X
  • Ironport-phdr: A9a23:sc/+ZhzxJOh2XzrXCzJqwFBlVkEcU1XcAAcZ59Idhq5Udez7ptK+Z heZuKom1QaQFazgqNt8w9LMtK7hXWFSqb2gi1slNKJ2ahkelM8NlBYhCsPWQWfyLfrtcjBoV J8aDAwt8H60K1VaF9jjbFPOvHKy8SQSGhLiPgZpO+j5AIHfg9q52uyo+5DeYQpEiCegbb9vM R67sRjfus4KjIV4N60/0AHJonxGe+RXwWNnO1eelAvi68mz4ZBu7T1et+ou+MBcX6r6eb84T aFDAzQ9L281/szrugLdQgaJ+3ART38ZkhtMAwjC8RH6QpL8uTb0u+ZhxCWXO9D9QLYpUjqg8 qhrUgflhikHOTAn7W/Zict+g61HrxyuvBF/34zZbZuJOPdkYq/RY9UXTndBUMZLUCxBB5uxY 4UND+oGO+ZYror9qEUKrRSgGwahH+zvyjpSiX/32a02yfguEQbD3AAuAtkDt3bUrNLzNKcTU uC60q3IwivdYP5N1jf97ZLHchElof2WQb1wds/RxFApGgjYgVqetZbrMCmJ1uQRrWeb9exgW PqxhmM7pA98vjqiytkjh4TXmo8Yzl7J+Th5zYg1K9O0Vk92bMK5HJZMuC+XNZZ6TM0hTmxnt is0xKEKtJ2mcCUWzpks2hDRa/uCc4eS4xLjUv6cIS5lhH1/frK/mwy98U26xe3zTMa10VdKr ixbndXWsXANzRPT586aQfV+5keswSiD2xzX5+1eIk05lbDXJ4Mgz7IsjJYfrEbOEjPulEnoj aKaalgo9+215+njfrrro5CROo5ohg3iN6kjlNKwDOs9PwQQQ2SU5/iz2bj98ULlTrVKgPg7k qfHv53bJMkWo620DxNJ3ok47Ru0Ei2o384CnXYdKVJIYBKHgJbtO1HJOP34CO2wg1WokDty3 vDGIqDtDozDLnTekrrtYaxx60FbyAo0wtBf44xbBqsdL/L0X0/9rN3YDhknPAyo2+vrFslx2 4cEVW+MAqKVKr7evF6U6u41PuWBZpMZtC74K/c/5v7uiXE5mUUafamsxZYXane4HvJnI0Waf 3XshskOHnkRswoxSezlklyCUTpJa3muWKI84yk3CIS9AojbXICinKSB3DunHp1Rfm1KF0iAE W30eIWcR/cMdCWSL9d9nTwDTLitUpMu1RWztADh0LdnNerV+igAtZ35ztR15uvTlQsz9TNuF cid3XuNHClImTYDQCZz16RiqwQpwVCalKN8nvZwFNpJ5voPXB1sZrDGyOkvQdL1XAPCc9OER X6pR9ynBXc6Sdd7i4sMZEB8GNimgx3r0C+jArtTnLuOUs9nupnA1mT8cp4ug03N07Ms2gFOq qpnMGSngvU67A3PH8vSlF3fka+2dKMa1SqL9WGZzGPIslsLGBVoX/DjWnYSLlDTscy//lnLG r2pD7UkPw9MxOaNL6JLbpviilAVDOz7NoHmanmq03y1GQ7Ow7qNaITwfGBI3iLbCUsJlw0e1 XmDPAk6QCympjGWFyRgQHToZU6k6uxisDW7Q0szmhmNdFFk3qGp9wQ9gPWdT7YKwutBtn5+8 3N7G1Gy29+QAN2Fz+Z4VINbZ951oFJO1GaC8hd4IoTlNKd6wFgXbwVwuUrqkRRxEIRJ18Yw/ jssy0JpJKSU3UkkFXvQ1I3sOrDRNmj5/Qy+I6/Q1FbE1d+K+6AJoP0molTntQutGwIs6XJim 9VS1nKd4N3NAm9wGdrzVUA29BV+qrzybSw05oeS3nppcOG1vjLEx9M1Fb490B/zN9xbMa6CC ErzC5hAX5noeLFswgbxKEtbZLM3luZ8Jc6tevqY1bT+Oe9hmGnjlmFb+MVm1VrK8SNgS+nO1 pJDwveC3wLBWS2v6TXp+s3xh41AYikfW2Slzi2xToxWYKxxcIIGBE+hJsS2wpN1gJunCBs6v BazQkgL3sOkY0/YbVv73A5d0UkaiXOikCq8iTdzlnt65rra1yvIzeP4cRMBMWMeX2hug2DnJ o2shswbVkylB+QwvCOs/l2yh61SpaAkanLWXV8NZC/uaWdrTqq3sLOGJc9J8pIh9ytNAqywZ lWTS7i1pBV/sWurHWxYxTM2czynkpr8lh1+zmmaKT5/oWHYdsd52RrErIaEFLgBg3xfGnE+0 GaPTlGnd8Gk59CVi4vOvoXcHyq6W5tffDOqhYKMuS2n5HF7VBi2nvS9gNriQkAx1S720cUvV D2d9k6tJNm2kf3kaaQ+IRE7YT20o9B3EYx/jIYq0ZQZ2HxBw46Q4WJCimDrd9NSxaP5anMJA z8N2d/cpgb/iygBZjqEwZz0UnKFz45vfd6/NykU3SQ87M1OBaq847lNnC8zqV2951G0A7A1j nIGxP0i5WRPyeMOvgsuwyGQD5gdGEBZOWrnkBHCvLXc5O1HIW2od7a3zk93m9usWaqDrg9rU 3H8Yp4+HCV045Y3IBfW3Xb08I2hZMjIYIdZqEiPixmZxbswStp5hr8QiCFgI264oXA117txk 0l1xZ/j9Imfdzc2oeTgU0YebGGqIZtUoG2ljL4CzJjKmdr0RdM4RG1NBNyxHJfKWHoTrai1a VjISWVm7C/dQf2FRUee8Bs08SyJScz6cSHPYiFel40qRQHBdhMFxllIGmxrxNhhUVn6oa6pO EZhumJOuhih8EYKkqQwcEChGmbH+FXxMmdyEcfAakoQtkYYvg/UKZDMt70oWXgJotv56lTKc zL+BUwADHlVCBbcVhazY//3v4mGq6/BWaK/N6ecO+zQ77EOEa7Zn9T3ldI3tzeUapfVZyckV aZqnBEZGyg+QpW8+X1HXSUTk2ilg9ezghC692U3q8m+9K+uQwfz/c6UDKMUN9xz+hewiKPFN uiKhS8/JywKnpULjWTFzrQSxjtww2lnaiWtHLIctCXMULOYm6lZCAQeYj9yM80A5rw13w1EM 8rWwt3v0bswgvkwAlZDHVvv/6PhLdQNOH24PUjbCVyjMb2HIXjS35iyb/rjEftfi+JbsxD2s jGeUgfiMjmFizj1RkWvPOVL30T5dFRVvICwdAooCHC2Foq3LE3mdoYp1XtvnuVn4xGCfXQRO jV9bU5X+7iZ7CcDx+56B3QE9X19a++Nhyee6eDcbJcQq/piRCpuxIc4qDw3zaVY6CZcSbl7g izX+5RspFenkeSLxzdPXx9HqzINj4WO9xYHW+2R5txbVHDI8QhYp32XEAgPrsB5B8fHvqlRz p3WiPu2Jm4dq5Tb+swTA8WSI8WCeilEU1KhCHvfCw0LSiSuPGfUihlGkf2cwXaSq4Aztpnmn JdmolBzW1k8F/dcAUNgToVqyHZfWzollfuCkJdN6yPh9F/eQ8JVup2BXfWXU62HwNOxgrxNZ h9OyrT9f9x7Cw==
  • Ironport-sdr: RaCiPaQJfkW4TBjzt+sxoINuCwFDzidlrh7mliT6/CARTLzRVB6qK0R4d9uEpG62jXn4rs/3UP ScNiv1bwMHSMplEgpqFmT86NYc1+H1OSuQ8cSfLyJL+0/fjB788ero/6fl10EpXmMJ46zw1Zp1 b4VNjdl+2hRMee8c0cXZoaT2wSdV26mRS7TYGmqOEIrR2dgOoxWOYag8ZOjPEWsdXsn6IxGu91 W77r+tmafEE5Bje1vH6biWbcAdO8DMaDENI4T1ITi6TYRsx1M2E7fDnzDsgCEH0Bm7/TD7PNDc dlCcTINwIAVBzhwHWiSnHzOm

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