coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Quanta magazine article on Lean (with mentions of Coq)
- Date: Sun, 11 Oct 2020 20:46:51 +0200
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=gaetan.gilbert AT skyskimmer.net; spf=Pass smtp.mailfrom=gaetan.gilbert AT skyskimmer.net; spf=None smtp.helo=postmaster AT relay11.mail.gandi.net
- Ironport-phdr: 9a23:tBhzaRIe0/tPdYPqfNmcpTZWNBhigK39O0sv0rFitYgfKfjxwZ3uMQTl6Ol3ixeRBMOHsq0C1red6vqxEUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCe/bL9oLBi7rQrdutQIjYZmN6081gbHrnxUdupM2GhmP0iTnxHy5sex+J5s7SFdsO8/+sBDTKv3Yb02QaRXAzo6PW814tbrtQTYQguU+nQcSGQWnQFWDAXD8Rr3Q43+sir+tup6xSmaIcj7Rq06VDi+86tmTgLjhSEaPDA77W7XkNR9gr9FrhKvpxJxwIDab4+aO/V8YqzTcsgXRXZCU8tLSyBNHo2xYokJAuEcPehYtY79p14WoBW/HwarGP/vxSVOhnDu3KM60uAhHhrY0ww6A9IFrXPZrNrvO6gMTeC61q/IwS/Mb/NX3Tfy85bHcgo9ofyXRrJwcsrQyVIsFwPEi1WQrJLqPymP2uQLrWeb8/NtWOSygGEotw9/uCKgxtswiobXnIIVzEjJ+Th6zYg1OdG1VEB2b96kHZVQuC+UN4R4T8AmTmxquCg3xLILtIOlcCUE1Zkpxx7SZfKbfoWU4hztW+ScLSp2iX9jZbmxiRGy8U26xe39UMm5yE9KrjdfndnKqnACzRnT5dKISvRn/0ah2DCP2B7J5uFDO0A0mqzWIIMizL4ojpcfr1nPEy3slEj0kKOabFgo9+qr5uj9fLnrqIKQO5dphgzwPakigNGzDOAiPgQTXWWW/f6w2KDj8ED5RrhBk+c4nbPDsJ/AIMQWvq65DBFR0oYk8xu/FSmp0NACkngHMV5JZQiLj43zNFHPJPD0F/i/jE6qkDh2xvDKJLvhDYvRLnTbkbfhe6hy61JExQYt0NxS5YhYB7MdLP7pR0P8tt/VAgUnPwG63urrENB92ZkfWWKLDK+ZKqTSsVqQ6+IgOeaDepMVtyz7K/Q/6P7ujHs5lkQDcqmzwZsac2u4HvdmIkWCYnrsg9IBEWIUsQokVuDqjkONUSJLa3aoQ608/i07CJ6hDYrbWo+th6WB0D6nEZ1Se2BJEUuBEWzodoWBQ/cDcjieIs5nkjweVLiuUZUt1R+0tFyy970yJe3NvyYcqJjL1d5v5uSVmwth2yZzCpGy2uKRRmdDsWIMTTIswOgrrkVw1l6Fl6d5h/ZVD8B7/PBYSQQ7MJvR1ap8BsykCVGJRcuAVFvzGobuOjo2VN9km4ZSMXY4IM2ri1X45wTvG6UczuLZH58l6aHd2n38PYB7xmqUjPB83WljedNGMCidvoA69wXXANSVwV+Uk6+7LP1a2SfM8CGMxGyCvQdeXRIiCfyUD0BaXVPfqJHC3m2HSravDbo9NQ4Yl5yZKbpRadzsiFhcAvHuJIaHbg==
see zulip
Gaëtan Gilbert
On 11/10/2020 19:44, jonikelee AT gmail.com wrote:
https://www.quantamagazine.org/building-the-mathematical-library-of-the-future-20201001/
About Coq, it says:
Coq users have formalized a lot of mathematics in its language, but that work
has been decentralized and unorganized. Mathematicians worked on projects
that interested them and only defined the mathematical objects needed to
carry their projects out, often describing those objects in unique ways. As a
result, the Coq libraries feel jumbled, like an unplanned city.
“Coq is an old man now, and it has a lot of scars,” said Mahboubi, who
has worked with the program extensively. “It’s been collaboratively
maintained by many people over time, and it has known defects due to
its long history.”
- [Coq-Club] Quanta magazine article on Lean (with mentions of Coq), jonikelee AT gmail.com, 10/11/2020
- Re: [Coq-Club] Quanta magazine article on Lean (with mentions of Coq), Gaëtan Gilbert, 10/11/2020
- Re: [Coq-Club] Quanta magazine article on Lean (with mentions of Coq), jonikelee AT gmail.com, 10/11/2020
- Re: [Coq-Club] Quanta magazine article on Lean (with mentions of Coq), Gabriel Scherer, 10/12/2020
- Re: [Coq-Club] Quanta magazine article on Lean (with mentions of Coq), Hugo Herbelin, 10/12/2020
- Re: [Coq-Club] Quanta magazine article on Lean (with mentions of Coq), Gabriel Scherer, 10/12/2020
- Re: [Coq-Club] Quanta magazine article on Lean (with mentions of Coq), jonikelee AT gmail.com, 10/11/2020
- Re: [Coq-Club] Quanta magazine article on Lean (with mentions of Coq), Gaëtan Gilbert, 10/11/2020
Archive powered by MHonArc 2.6.19+.