From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.140.38.69 with SMTP id s63mr4318891qgs.6.1465739790816; Sun, 12 Jun 2016 06:56:30 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.36.96.135 with SMTP id i129ls673938itc.8.gmail; Sun, 12 Jun 2016 06:56:30 -0700 (PDT) X-Received: by 10.98.26.193 with SMTP id a184mr4547865pfa.12.1465739790115; Sun, 12 Jun 2016 06:56:30 -0700 (PDT) Return-Path: Received: from outgoing-tmp.csail.mit.edu (outgoing-tmp.csail.mit.edu. [128.30.2.206]) by gmr-mx.google.com with ESMTP id v62si392492itf.3.2016.06.12.06.56.30 for ; Sun, 12 Jun 2016 06:56:30 -0700 (PDT) Received-SPF: pass (google.com: domain of she...@csail.mit.edu designates 128.30.2.206 as permitted sender) client-ip=128.30.2.206; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of she...@csail.mit.edu designates 128.30.2.206 as permitted sender) smtp.mailfrom=she...@csail.mit.edu Received: from dhcp-18-189-48-43.dyn.mit.edu ([18.189.48.43]) by outgoing-tmp.csail.mit.edu with esmtpsa (TLS1.0:DHE_RSA_AES_256_CBC_SHA1:256) (Exim 4.82) (envelope-from ) id 1bC5sI-0005Y6-Tx; Sun, 12 Jun 2016 09:56:27 -0400 Content-Type: text/plain; charset=utf-8 Mime-Version: 1.0 (Mac OS X Mail 9.3 \(3124\)) Subject: Re: [HoTT] How to make software without money From: Ben Sherman In-Reply-To: Date: Sun, 12 Jun 2016 09:56:25 -0400 Cc: =?utf-8?Q?andr=C3=A9_hirschowitz?= , "HomotopyT...@googlegroups.com" Content-Transfer-Encoding: quoted-printable Message-Id: <3D8A7143-5B34-4897-87E6-102B4C207686@csail.mit.edu> References: To: Andrej Bauer X-Mailer: Apple Mail (2.3124) I feel that I should mention some recent developments that are relevant to = this discussion, at least with respect to Coq. Firstly, Paul Steckler recently joined MIT. He works full-time, as an engin= eer, towards improving Coq as a software system for its users (see the job = posting here: https://groups.google.com/forum/#!topic/fp-syd/wiff-ks5yVw). = I don't know exactly where the funding for his position comes from. Secondly, Yves Bertot announced earlier this week at the DeepSpec workshop = in Princeton (http://deepspec.org/events/) the creation of the Coq Consorti= um, which will be an organization dedicated to the improvement of Coq as a = software system for its users. Industrial and academic institutions can pay= an annual fee to the Coq Consortium, which will serve to fund full-time en= gineers to work on improving the Coq system, and these engineers will prior= itize the goals of those who fund them. I think the details are still being= worked out. (Again, I am not knowledgable about what funding sources acade= mic institutions can use to pay into the Consortium.) The goal is that with the Coq Consortium, INRIA researchers will be freed t= o focus on research-relevant aspects of Coq, and Coq users will be able to = use a software system whose quality can only be made possible by the attent= ion of full-time engineers. I am personally hopeful that this strategy will= work favorably for all those involved! > On jun 12, 2016, at 7:05 AM, Andrej Bauer wrote: >=20 > While the efforts expanded on Coq and Agda are truly impressive and > chivalrous, both pieces of software compare poorly to something like > Mathematica in terms of software quality (documentation, professional > GUI design, technical support, cloud support, etc.) This is not a > criticism of the Coq and Agda teams, just an observation which in > Slovene could be summarized by the phrase "that's the music you get > for the money you paid". >=20 > Also, I am not trying to start a war with the lurking Knights of the > Open Source. I am just saying we have no idea how to bring open-source > mathematical software to the level of professional software without > sacrificing the careers of several PhDs and at least one tenured > professor. >=20 > With kind regards, >=20 > Andrej >=20 >=20 >=20 > On Sun, Jun 12, 2016 at 12:55 PM, andr=C3=A9 hirschowitz = wrote: >> Hi, >>=20 >> I have been thinking to this issue for years (decades?). In France we ha= ve >> this research agency INRIA which has been supporting the Coq project for >> decades, leading to a fairly "good quality software" (in my opinion). Sa= y >> twenty years ago, the Coq project was targetting the computer science >> community and was not ready to "attack" the mathematical community. From >> this side, the picture seems much better nowadays. >>=20 >> A possible strategy toward the investment of the mathematical community = is >> as follows: >>=20 >> ------------------------ >>=20 >> 1- create a body tying (part of) this community with for instance (part = of) >> the Coq project (and/or the Agda project, about which I know little). >>=20 >> 2- obtain specific funding from a Research Agency (NSF, CNRS?) for partl= y >> formalized PhD fellowships, together with companion funding for the >> technical support (eg from the Coq team) to the (partial) formalization. >>=20 >> 3- obtain good applications, coming from ouside this community. >>=20 >> 4- select the winning applications regarding both the interest of the na= ked >> thesis, and the feasability of the (partial) formalization. >>=20 >> 5- help collectively the success of each selected project. >>=20 >> 6- Write assessments in particular for the formalization efforts of thes= e >> newage doctors, so that they win positions whenever they deserve. >>=20 >> --------------------------- >>=20 >> I leave it here. >>=20 >> ah >>=20 >>=20 >>=20 >>=20 >> 2016-06-12 10:04 GMT+02:00 Andrej Bauer : >>>=20 >>> Apologies for a slightly off topic post, but I think it is relevant to >>> many people on this list. >>>=20 >>> I just looked at some slides by William Stein, the author of Sage (an >>> open-source alternative to Mathematica) at >>> http://www.smbc-comics.com/index.php?id=3D4127 >>>=20 >>> The conclusion is: it's impossible to make good quality software in >>> academia because there isn't enough money and because making software >>> doesn't give one any academic credit. >>>=20 >>> I am afraid formalization of math might fall into the same category, >>> unless we somehow elevate it to a "true science" level. A great deal >>> has been done in this respect recently by projects lead by Gonthier, >>> Hales and Voevodsky, but is it enough? Are we even making a dent? >>>=20 >>> At my department, for instance, the folk knowledge propagated from one >>> generation to another is that "someone" formalized "Landau's book" (I >>> suppose it was the Automath formlaization of Landau's Grundlagen der >>> Analysis by Jutting) which proves that "it can be done" but is >>> otherwise an intellectually barren exercise without academic value. I >>> still remember one of the professors saying this to the whole class >>> when was an undergraduate. >>>=20 >>> With kind regards, >>>=20 >>> Andrej >>>=20 >>> -- >>> You received this message because you are subscribed to the Google Grou= ps >>> "Homotopy Type Theory" group. >>> To unsubscribe from this group and stop receiving emails from it, send = an >>> email to HomotopyTypeThe...@googlegroups.com. >>> For more options, visit https://groups.google.com/d/optout. >>=20 >>=20 >=20 > --=20 > You received this message because you are subscribed to the Google Groups= "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an= email to HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout.