coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Quanta magazine article on Lean (with mentions of Coq)

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