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: Ralf Jung <jung AT mpi-sws.org>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Lamport on TLA+ in Quanta, with Coq mention
  • Date: Tue, 17 May 2022 20:04:39 +0200
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jung AT mpi-sws.org; spf=Pass smtp.mailfrom=jung AT mpi-sws.org; spf=None smtp.helo=postmaster AT juno.mpi-klsb.mpg.de
  • Ironport-data: A9a23:v9eQLqIVvKgAx3E3FE+RB5MlxSXFcZb7ZxGr2PjKsXjdYENS1TxVm DFJUG2BPvjZY2H8c413bI23904PusCEyYUyQQYd+CA2RRqmi+KVXIXDdh+Y0wC6d5CYEho/t 63yTvGacajYm1eF/k/F3oDJ9CU6jefSLlbFILas1hpZHGeIcw98z0M68wIFqtQw24LhXlrS4 YmaT/D3YTdJ5RYkagr41IrY8HuDjNyq0N/PlgFWiVhj5TcyplFNZH4tDfnZw0jQHuG4KtWHq 9Prl9lVyI92EyAFUbtJmp6jGqEDryW70QKm0hK6UID66vROS7BbPqsTbJIhhUlrZzqhk882w 81knreKSQ4rEJeUicpAbil5DHQrVUFG0OevzXmXs9GVyAvDa3qpwPF1BgczJYJe9usf7WNmr KdJbmlcKEDdwb7uqF64YrEEasALLtTtM6saonAl1i7CS/E8TvgvRo2TuYQGhGtt3KiiG97Pd tcDTQtmYi7qID5/GFg6KdUknfa30yyXnzpw8gvO/PFnsgA/1jdZ27/0ddHRZ9aiXtRQhk/ep 2Tc/m2/DAtyCTCE4TiY9HXqg/fO2CD/Q4hUEaW3sPJn6LGO+oANIBEJElCjiNKSsE63Wfxlc 106pxcejLdnoSRHUeLBdxG/pXeFuDsVVNxRD/A25WmxJkz8vV3x6o8sEGUpVTA2iCMlbWFzj A7YxLsFERQ+7OzMERpx45/O9WvaBMQDEYMVTQMpJTbpDvHhvYc0yBfXT5NgFLW/yNjtFnf8z lhmTRTSZZ1M1abnNI3ioDgrZg5AQLCUFGbZAS2KBwqYAvtRPtLNWmBRwQGzAQx8BIiYVEKdm 3MPhtKT6usDZbnUynHXH79QTOv3uq/dWNE5vbKJN8Z8n9hK0yH/Fb28HBkkexkB3jssKWewO BOC52u9GrcNYyf7MMebnL5d++xwlPO5ToS0PhwlRtZDf4Rqfw+K52lgYlSL1GDwlkc3l6wjK /+mnTWEUh4n5VBc5GPuHY81iOZzrghnnDO7bc2lk3yPjOTPDFbIGeZtGAbfNYgRsfLbyC2Lq Iw3H5XRlH1ivBjWP3O/HXg7dw5adBDWxPne9qRqSwJ0ClA9SDx9WqaInOxJlk4Mt/09q9okN 0qVAidwoGcTT1WeQelTQnw8Or7pQ7hlqnc3YX4lMVqygiFxZJ6uqbwAbN0wZ7Z+rL5vyvt9T v8kfcScA60WEG6fom5HMsXw/N54aRCmpQOSJC75MjIxSJhtGl7S8dj+cwqzqSQDV3LltcY3r 7C6+BncRJ4PG1ZrAMrMMav9ykuw+GMCg6R1RUSReotff0Dl8Y5LLS3tj6ZueZtUcE+ZmWeXj l/EDw0ZqO/Bp54O3OPI3a3U/Z20F+ZeH1ZBGzWJ57iBMySHrHGoxpVNUbrVcD3QCDH09aGla bkHxv3wKqdfzlRXtY06Fq5qiKE6/NGpoqdViAhpRS2ZY1OuA7JmA3+HwcgW6vwTnOAE41PuV xLd4MReNJWIJNjhTgwbKj0lWfvdh/sarTnl6/locl7x4zV6/efZXBwKbQWMkiFUMJB8LJghn bU6oMcT5gHj2AAmNM2K0nJd+2iWdCRSUbghsdcfGI6uiQ4wwBdHeZOaBiKvuMODbNBFM08LJ D6IhfOe1uoGmReYKyI+RSrXwO5QpZUSoxQUnlUMEFS+hYSXjPEA3CpX/GllVQ9S1BhGjrx+Y zA5K01vKKyS1D50n8wfDXu0EgRMCRDxFpYdELfVeLk1jnVEV1Ah6EU/JOCKukUB8idfeiNRu rSAxyDpXF4GuS03MjQaASZYRz7LFLSdNTEuXOiiB8XABIYhJz3/jcdCoEIW/gD/D5pZaFLv/ IFXESUZVUE/HSsIouggFJLc0q4fIPxByKquXtk5lJ408arglP1eFNRAx41dui+AGhASzXKFN g==
  • Ironport-hdrordr: A9a23:dKQGB635wF/+9ovNfuhCCAqjBIkkLtp133Aq2lEZdPU1SL3gqy nKpp8mPHDP+VEssR0b6LO90dC7IU80lqQFh7X5X43OYOCOggLBRr2Ki7GSoQEIcBeOktK1u5 0QFpSWP+edMbGqt6fHCFjRKbgdKIfuys+Vuds=
  • Ironport-phdr: A9a23:Exh1IBGzs6CK+Ws13vS5H51Gf7pHhN3EVzX9CrIZgr5DOp6u447ld BSGo6k31xmUAs6Csq8MotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7G MNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+5ZPebx9IiTe/br9+M Qi6oAXMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2Q rxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v6 bpgRh31hycdLzM382/ZhcN+g6xGvhyhqRxxzIzIb4+aL/d+YqHQcMkGSWZdUMtcVSpMCZ68Y YsVCOoBOP5VoZXnqFsKoxu1GA2iBP7pyj9Hm3T72q860/knEQHJxwEgGsoOsHXNoNXuOqYSS vq5zK7SzTXMdv5b3yr254fUfB47u/6MQa5wftTLyUkpDw7JklGdpIzlMT6I2ekAsGuW4uluW O6ylWIppB98ryWzy8owhITEiIwbx0zY+Ch4zog4JN22RVNlbdOgEpZcqz2WOo1rSc0sRGFov Tw1yrwAuZOjZSgK1Y4oxxjDa/OddoiH+B3jW/yQIDd5gnJqZqizhxGo8Uiv0uH8TNO70FJEr ipHiNXDq24C2hrO4caEUvtw5lqt1DiL2gzJ9+1JJVo4mKnaJpI7zbM8ioIfvEbHEyPshkn7g 66bel859uWo5OnreKjqq5CBO4JylwrwKL4hmtalDuQ9KgUOX3aU+eC71LD7/035XbNKjvosn qncqJDaJN0Xpq29Aw9OyYkv8RO/Dy+p0NgCgHYIMkpJeBOBj4f3J1HDOO30APm7jli2jTtmw +rKM77gD5nXIXXPjK/tfbNn5E5dzAozw8pf55VRCrwZIvLzR0nxtNPDAx88Kwy0wv/rCM5z1 4MFQ26PBbWZMKzKvV+O/e0gO/OMa5MNuDbhN/gl4ObjgWIhlV8HYaapxYcXaGy/Hvl+P0qZZ mPsjs4dHmcOowoxV/fniEaCUD5Wf3a9Rbgw5jA9CIK8DIfMXJqhgLKb3HTzIpoDbWdfT1uID H3AdoOeWv5KZjjBDNVml2k+XLyvA6080x7m4A3nzbVPK/LVvzYHrtTkztcjtL6brg076TEhV 5fV6GqKVWwhxgvgJhcz1aF7+glmz0ublLN/m7peHMBS4PVAVkE7M4Tdxqp0EYO6QRrPK/GOT lvuWdC6GXcpVNtkwcIIbG54A9TnlQ/YmS2wDOxdjKSFUaQ96bmUxH3tP4B4wnfC2rMmigwkX 81AHWi+h+tk6BOVAJTGwA2Cj6j/U6Ma0WbW8Xubi2qDuEYNSAlrTaDMRmwSfGPUsNL+oEbaT vqtDa8tdA5ZxoiOJ8Omc/XPilNLDLfmMdXaOCeqnnuoQA2P3vWKZZbrfGMU2GPcDlIFmkYd5 yTOMw92HSqnr2/EaV4mXVvyf0Ph9/V/o3KnXwc1yQ+NdUhoy7uy/FYcm/WdT/oZ2r9Mtj0mr n14G1O03tSeDNTlxUIpfrhabvs4+FYCzn3C8QtnMd3oLqxvgEIfbxUip1nnhF18DoRNl9Rvr Wt/lVEjb/vJlgMfMW/AjvWScvXNJ2L//Q6icfvT01Dai5ON/7sXre8/sxPltR2oEUwr9zNm1 cNU2j2S/MavbkJaXJTvX0Iw7xU/qavdZ3x35Z7S2lVpKajxqSDZndUzC6F2r3ToN8caK66CG ALoRocYGs6hAOkymh2ycQlCO/pdvv18L4atcP2I37SuNeBrkWe9jGhJ14t611qF6yt2TuOgM 48t+/iDxUPHUj79iAzkqcXrgcVfYilUGGOjyC/iDYoXZ6tofI9NB338a8Gww9x/gdbqVRs6v BahGlUJ8MqxeF+JcEe72hdfnUgaun2onyKkwic8ymp46PPOmnyQhbi6PBMccnZGXmxjkUvhL cCvgtYWUVLpCmph3Bqp6EDmxrRK8aF2Lm3dW0BNLGD9K2BvVLf1t6LXOpUersp593UJFrjkM jX4AvbnrhAX0j3uBT5bzTE/LHSxv4nh2gd9kCSbJWpyq3zQfYdxww3e7ZrSX600vHJOSS9mh D3QHlX5McOu+IDelYrFvci7T2PkTYJINy7xwsnT0UnzrX0vGhC5k/2pz5flDA41+Srj1pxxS j6OqwzzKNqjx+GxNuRpeVNtDVn35p9hG41wpYA3gYkZxXkQgpjGmBhP2Xe2K9hQ3rjyKWYcX TNeicCA+xDrgQcwZmLM3Y/yUW+Rh9dsd8XvKH1DwToztqUoQO+dvrxJhyIzp0K56AHVevI7m y8Sj/cjoHdIgfwPv0wo1iTYAbQJFw9dJSOqmxntjZj2pfdPYHuzdv61zEs7ntS6BveHug4aV Huxc8UrBSh06sI5NUrNlX738YuifcHfK94e03/c2x6SjfVNKY48jLwPnSsiOmbmtzsg0+F9g REm1MOiu5OKKmlq+uS8Gh8dNTnubYUW4j6rgasWyc+S28rH8oxJPDINUdOoSPupFGlXrvH7L 0OVFyV6rH6HGL3ZFAvZ6UF8rnuJHYr5f3eQbGIUy9lvXnz/bARWnRwUUTMmn5U4ChHixcrvd 1187ywQ4ViwowVFy+ZhPR3yGmnFowLgZjAxQZmZZB1Yi2MKr1/SKtCb5/lvEjtw/ICnq0qIM m3eZABTBycMQkPCC12idrii6N/c8vSJU+qzK/ydBNfG4edaVvqO2deuyt4/pGfKb5TJbickU 6VovygLFWp0EMnYhTgVHikeliaWKtWeuA/54Spv6Ma27PXsXgvro4qJEbpbd9t1qHXUye+OM fCdgCFhJHNWzJQJkDXK1b4Q9FsKimR1aCLrFq4P/32oLuqYiupMAhgXZjkmftNP9L451xJRN NTziM7z0fh9lv9wCFNeXxrkgs7vacFAcATffBvXQU2MMrqBPzjCxcr6NLi9RbNnh+JRrxSsu DyfHicL3xyBij/uERW3MKRPiDqRehlGt8exf0Q1YYAGZNf+a1igL8Qxiic5k+VcbpziMHYdd CNjaAVKtLLCtEtl
  • Ironport-sdr: J+YtNxmrbMgfUg8zg0DOv9N5Kwrr0sOfFV4OKcKQ3HOtS6Ous0SGRW0aEjds9iaCwjwrk+Uoqz 8BCTrX4yM9vH6MKAPo8a+d9gZBOw600QNqU1GfnK9GzQ9gLE/tRw7Yd2GMxoWqwG6wD04Rg6eh 7A6UUe2TIDbw1zO/9uugFjqjWSdtHO+8+TE/Qf0/+79yho0g01Nkmrnl+JhTashNT0EWI5JbGE YV1s1phJvp4S7Snp+F2J6w/oABQ6HmWQE58P2Tb6lhP3MdyvFjAk6t1KOzqqshlLr0xEC7cVGV A3mvRqLBE1bBabLjzcLkcxq1

I would say TLA+ was designed to prove properties of *models of* their
systems. ;)

; Ralf

On 17.05.22 19:36, jonikelee AT gmail.com wrote:
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.




--
Website: https://ralfj.de/research



Archive powered by MHonArc 2.6.19+.

Top of Page