Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • 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.”




Archive powered by MHonArc 2.6.19+.

Top of Page