From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.237.49.134 with SMTP id 6mr8241711qth.20.1465732261358; Sun, 12 Jun 2016 04:51:01 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.9.69 with SMTP id 63ls885679otp.32.gmail; Sun, 12 Jun 2016 04:51:00 -0700 (PDT) X-Received: by 10.157.10.71 with SMTP id 65mr8121990otg.48.1465732260760; Sun, 12 Jun 2016 04:51:00 -0700 (PDT) Return-Path: Received: from data.hamecon.telecom.uqam.ca (mail2.uqam.ca. [132.208.246.165]) by gmr-mx.google.com with ESMTP id n132si1247735ywb.1.2016.06.12.04.51.00 for ; Sun, 12 Jun 2016 04:51:00 -0700 (PDT) Received-SPF: pass (google.com: domain of JOYAL...@uqam.ca designates 132.208.246.165 as permitted sender) client-ip=132.208.246.165; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of JOYAL...@uqam.ca designates 132.208.246.165 as permitted sender) smtp.mailfrom=JOYAL...@uqam.ca Authentication-Results: data2.hamecon.telecom.uqam.ca; spf=None smtp.mailfrom=joyal...@uqam.ca; spf=None smtp.helo=postm...@Avis.gst.uqam.ca Received-SPF: None (data2.hamecon.telecom.uqam.ca: no sender authenticity information available from domain of joyal...@uqam.ca) identity=mailfrom; client-ip=132.208.246.209; receiver=data2.hamecon.telecom.uqam.ca; envelope-from="joyal...@uqam.ca"; x-sender="joyal...@uqam.ca"; x-conformance=spf_only Received-SPF: None (data2.hamecon.telecom.uqam.ca: no sender authenticity information available from domain of postm...@Avis.gst.uqam.ca) identity=helo; client-ip=132.208.246.209; receiver=data2.hamecon.telecom.uqam.ca; envelope-from="joyal...@uqam.ca"; x-sender="postm...@Avis.gst.uqam.ca"; x-conformance=spf_only X-Cloudmark-SP-Filtered: true X-Cloudmark-SP-Result: =?us-ascii?q?v=3D2=2E1_cv=3DHsTWYxnS_c=3D1_sm=3D2_tr?= =?us-ascii?q?=3D0_a=3DzdVg5ADNf/sAC0uRWyjItQ=3D=3D=3A17?= =?us-ascii?q?_a=3DSgJDDHH=5FwjgA=3A10_a=3D8nJEP1OIZ-IA=3A10_a=3DpD=5Fry4oyN?= =?us-ascii?q?xEA=3A10_a=3D4RBUngkUAAAA=3A8?= =?us-ascii?q?_a=3DjM9pu8wBAAAA=3A8_a=3DQZ0zsqwyAAAA=3A8_a=3D1XWaLZrsAAAA=3A?= =?us-ascii?q?8_a=3DwQw91aaRdPqhiJNJOgcA=3A9?= =?us-ascii?q?_a=3DZuBT9lV-ChJe=5Frix=3A21_a=3D9wss4uQwgGAYy1kn=3A21_a=3DwPN?= =?us-ascii?q?LvfGTeEIA=3A10?= =?us-ascii?q?_a=3Dc4S9Whzb7AQA=3A10_a=3DHCwVASBe7R0A=3A10_a=3D=5FsbA2Q-Kp09?= =?us-ascii?q?kWB8D3iXc=3A22?= =?us-ascii?q?_a=3Dz6IKlSWrg7XnYVYzWFns=3A22_a=3DH64zJV-NxZ6a0dAiZeZv=3A22_a?= =?us-ascii?q?=3DnJcEw6yWrPvoIXZ49MH8=3A22?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A2COBQB3Q11X/9H20IRDGoM+Vn0Ggza5Y?= =?us-ascii?q?BcLgj6DNwKBHzwQAQEBAQEBAWUnhEoBAQEETh0OEAIBCA0EBAEBAQokMQEdCAI?= =?us-ascii?q?EAQcGAQQBBwwJAQOIDw4tvREBAQEBAQEBAQEBAQEBAQEBAQEBAQEciXGBA4QSE?= =?us-ascii?q?QEegyqCLwWIDIYaijuGBJF/hUWPbjUfggccgUtuAQYNiD82AX4BAQE?= X-IPAS-Result: =?us-ascii?q?A2COBQB3Q11X/9H20IRDGoM+Vn0Ggza5YBcLgj6DNwKBHzw?= =?us-ascii?q?QAQEBAQEBAWUnhEoBAQEETh0OEAIBCA0EBAEBAQokMQEdCAIEAQcGAQQBBwwJA?= =?us-ascii?q?QOIDw4tvREBAQEBAQEBAQEBAQEBAQEBAQEBAQEciXGBA4QSEQEegyqCLwWIDIY?= =?us-ascii?q?aijuGBJF/hUWPbjUfggccgUtuAQYNiD82AX4BAQE?= X-IronPort-AV: E=Sophos;i="5.26,461,1459828800"; d="scan'208";a="141374519" Received: from unknown (HELO Avis.gst.uqam.ca) ([132.208.246.209]) by data2.hamecon.telecom.uqam.ca with ESMTP/TLS/AES256-SHA; 12 Jun 2016 07:50:59 -0400 Received: from PLI.gst.uqam.ca ([169.254.3.160]) by Avis.gst.uqam.ca ([169.254.2.34]) with mapi id 14.02.0387.000; Sun, 12 Jun 2016 07:50:58 -0400 From: =?iso-8859-1?Q?Joyal=2C_Andr=E9?= To: Andrej Bauer , =?iso-8859-1?Q?andr=E9_hirschowitz?= CC: "HomotopyT...@googlegroups.com" Subject: RE: [HoTT] How to make software without money Thread-Topic: [HoTT] How to make software without money Thread-Index: AQHRxIECCgUnZpHbu0K4EUiFBcdA8J/l69uAgAAC5AD//8f0Pw== Date: Sun, 12 Jun 2016 11:50:58 +0000 Message-ID: <8C57894C7413F04A98DDF5629FEC90B138B933CA@Pli.gst.uqam.ca> References: , In-Reply-To: Accept-Language: en-US, en-CA Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: x-originating-ip: [132.208.216.81] Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 Dear Andrej, I am not an expert in software, but Agda and Coq offer something that Mathematica and Maple dont have: a calculus of proofs. Regards,=20 -Andr=E9 ________________________________________ From: homotopyt...@googlegroups.com [homotopyt...@googlegroups.com] on beha= lf of Andrej Bauer [andrej...@andrej.com] Sent: Sunday, June 12, 2016 7:05 AM To: andr=E9 hirschowitz Cc: HomotopyT...@googlegroups.com Subject: Re: [HoTT] How to make software without money 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". 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. With kind regards, Andrej On Sun, Jun 12, 2016 at 12:55 PM, andr=E9 hirschowitz wrote= : > Hi, > > I have been thinking to this issue for years (decades?). In France we hav= e > this research agency INRIA which has been supporting the Coq project for > decades, leading to a fairly "good quality software" (in my opinion). Say > 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. > > A possible strategy toward the investment of the mathematical community i= s > as follows: > > ------------------------ > > 1- create a body tying (part of) this community with for instance (part o= f) > the Coq project (and/or the Agda project, about which I know little). > > 2- obtain specific funding from a Research Agency (NSF, CNRS?) for partly > formalized PhD fellowships, together with companion funding for the > technical support (eg from the Coq team) to the (partial) formalization. > > 3- obtain good applications, coming from ouside this community. > > 4- select the winning applications regarding both the interest of the nak= ed > thesis, and the feasability of the (partial) formalization. > > 5- help collectively the success of each selected project. > > 6- Write assessments in particular for the formalization efforts of these > newage doctors, so that they win positions whenever they deserve. > > --------------------------- > > I leave it here. > > ah > > > > > 2016-06-12 10:04 GMT+02:00 Andrej Bauer : >> >> Apologies for a slightly off topic post, but I think it is relevant to >> many people on this list. >> >> 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 >> >> 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. >> >> 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? >> >> 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. >> >> With kind regards, >> >> Andrej >> >> -- >> You received this message because you are subscribed to the Google Group= s >> "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n >> email to HomotopyTypeThe...@googlegroups.com. >> For more options, visit https://groups.google.com/d/optout. > > -- 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 e= mail to HomotopyTypeThe...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.