From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.157.43.198 with SMTP id u64mr10448944ota.32.1465782820288; Sun, 12 Jun 2016 18:53:40 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.140.98.145 with SMTP id o17ls3122073qge.31.gmail; Sun, 12 Jun 2016 18:53:39 -0700 (PDT) X-Received: by 10.176.4.81 with SMTP id 75mr10561646uav.0.1465782819733; Sun, 12 Jun 2016 18:53:39 -0700 (PDT) Return-Path: Received: from mail-oi0-x229.google.com (mail-oi0-x229.google.com. [2607:f8b0:4003:c06::229]) by gmr-mx.google.com with ESMTPS id d11si35772ith.0.2016.06.12.18.53.39 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 12 Jun 2016 18:53:39 -0700 (PDT) Received-SPF: pass (google.com: domain of intov...@gmail.com designates 2607:f8b0:4003:c06::229 as permitted sender) client-ip=2607:f8b0:4003:c06::229; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of intov...@gmail.com designates 2607:f8b0:4003:c06::229 as permitted sender) smtp.mailfrom=intov...@gmail.com; dmarc=pass (p=NONE dis=NONE) header.from=gmail.com Received: by mail-oi0-x229.google.com with SMTP id u201so60566604oie.0 for ; Sun, 12 Jun 2016 18:53:39 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to; bh=yJCM7xHONZrVVeMm049MnLz7pdStg9C7TJvYO552ftk=; b=Hb02xDLSodhud0j+lHOQEwcNTccKEwjDi3RLoaSGowUgXHIiZrQXozTpv8vleMIVDx m/Wv7wkWBMd2yy+ASLJw3jiMXNrzhDzfEBnyR94U2D4+ip6TawKmlrEavTkf4t70v2Xl eVar19+nUEdoOq0ZNxka7ahum2CIEnFzTmJS2ZKkuHKeDQdWCUouKI7CmZdotFFFHFyp HZ0xojBUDQuLTpG1wVFCfwEasZqfbWLOdIrDybO0Uz72HCjxthqYSV9TQW6YRsDtooZX TGrC3Axa/Tm53OFTeI9cVQHpTuCXPZsniJCl8VpntTClHTGPAS1BPdxb0F/hVGOVgdh/ cV+Q== X-Gm-Message-State: ALyK8tIkWgphzlH+k4mW8YzB14t8Z7qICjaDCEfDbRO+GEVY2b6QDSeuICvyXZt6lpo/YX4EzdlEgqzVbjJaNA== X-Received: by 10.202.64.214 with SMTP id n205mr6534661oia.104.1465782819357; Sun, 12 Jun 2016 18:53:39 -0700 (PDT) MIME-Version: 1.0 Received: by 10.157.25.173 with HTTP; Sun, 12 Jun 2016 18:53:38 -0700 (PDT) In-Reply-To: References: From: Timothy Carstens Date: Sun, 12 Jun 2016 18:53:38 -0700 Message-ID: Subject: Re: [HoTT] How to make software without money To: Andrej Bauer , "HomotopyT...@googlegroups.com" Content-Type: multipart/alternative; boundary=001a113d672c440a2e05351f2895 --001a113d672c440a2e05351f2895 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable In the computer business, technologies which solve essential problems tend to survive; extensible technologies which solve essential problems tend to grow. When you look at the largest open source projects, the majority of the actual code tends to come from people working in large companies that depend on the tech stack. Linux, for example, has benefited enormously from IBM's investment of engineering-hours into the project. Ruby on Rails is another example, as are many other web-related frameworks. The SAGE math environment was a noble effort to displace MAGMA and similar systems, which were benefiting from code contributions from academia, but which remained commercial and not widely available. Later SAGE would evolve to compete with Mathematica and other math suites. Unfortunately, the essential problem being solved was a matter of taste-in-licensing, which is not always essential-enough for a project to take hold. Coq, Agda, Lean, etc, all solve an essential problem, namely that of providing a theory of higher-order machine-checked proofs. The implementations tend to be extensible, at least for experts. Different segments of the CS and math community are becoming aware of these tools and producing new, impressive artifacts all the time. Overall it's a small community, but it's growing. At the very least, the diversity of artifacts demonstrates that these tools are expressive-enough to be useful in many domains, not just in principle but in practice. Though it is currently difficult to apply these methods to problems of interest in industry, progress in the field of program logics is real and has lead to real tools (Infer, at least) with real users. The ability to prove properties of programs inevitably leads to the desire to prove properties of fairly technical programs, and in that way a bridge to more abstract, less-computery branches of math will emerge. An ecosystem will form, and pure research which contributes to this ecosystem will begin to take on its own appeal. Other paths to industry-awareness may exist, this is just the one I've been tracking. In my opinion, patience will be rewarded. -t On Sun, Jun 12, 2016 at 4:05 AM, Andrej Bauer wrote: > 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=C3=A9 hirschowitz = wrote: > > Hi, > > > > I have been thinking to this issue for years (decades?). In France we > have > > this research agency INRIA which has been supporting the Coq project fo= r > > decades, leading to a fairly "good quality software" (in my opinion). S= ay > > twenty years ago, the Coq project was targetting the computer science > > community and was not ready to "attack" the mathematical community. Fro= m > > this side, the picture seems much better nowadays. > > > > A possible strategy toward the investment of the mathematical community > is > > as follows: > > > > ------------------------ > > > > 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). > > > > 2- obtain specific funding from a Research Agency (NSF, CNRS?) for part= ly > > 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 > naked > > 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 the= se > > 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 > 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. > > > > > > -- > 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. > --001a113d672c440a2e05351f2895 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
In the computer business, technologies which solve essenti= al problems tend to survive; extensible technologies which solve essential = problems tend to grow.

When you look at the largest open= source projects, the majority of the actual code tends to come from people= working in large companies that depend on the tech stack. Linux, for examp= le, has benefited enormously from IBM's investment of engineering-hours= into the project. Ruby on Rails is another example, as are many other web-= related frameworks.

The SAGE math environment was = a noble effort to displace MAGMA and similar systems, which were benefiting= from code contributions from academia, but which remained commercial and n= ot widely available. Later SAGE would evolve to compete with Mathematica an= d other math suites. Unfortunately, the essential problem being solved was = a matter of taste-in-licensing, which is not always essential-enough for a = project to take hold.

Coq, Agda, Lean, etc, al= l solve an essential problem, namely that of providing a theory of higher-o= rder machine-checked proofs. The implementations tend to be extensible, at = least for experts. Different segments of the CS and math community are beco= ming aware of these tools and producing new, impressive artifacts all the t= ime. Overall it's a small community, but it's growing. At the very = least, the diversity of artifacts demonstrates that these tools are express= ive-enough to be useful in many domains, not just in principle but in pract= ice.

Though it is currently difficult to apply the= se methods to problems of interest in industry, progress in the field of pr= ogram logics is real and has lead to real tools (Infer, at least) with real= users. The ability to prove properties of programs inevitably leads to the= desire to prove properties of fairly technical programs, and in that way a= bridge to more abstract, less-computery branches of math will emerge. An e= cosystem will form, and pure research which contributes to this ecosystem w= ill begin to take on its own appeal. Other paths to industry-awareness may = exist, this is just the one I've been tracking.

In my opinion, patience will be rewarded.

-t=



On Sun, Jun 12, 2016 at 4:05 AM, Andrej Bauer <andrej...@andrej.com> wrote:
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 ge= t
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=C3=A9 hirschowitz <a...@unice.fr> wrote:
> Hi,
>
> I have been thinking to this issue for years (decades?). In France we = have
> this research agency INRIA which has been supporting the Coq project f= or
> decades, leading to a fairly "good quality software" (in my = opinion). Say
> twenty years ago, the Coq project was targetting the computer science<= br> > community and was not ready to "attack" the mathematical com= munity. From
> this side, the picture seems much better nowadays.
>
> A possible strategy toward the investment of the mathematical communit= y is
> as follows:
>
> ------------------------
>
> 1- create a body tying (part of) this community with for instance (par= t of)
> the Coq project (and/or the Agda project, about which I know little).<= br> >
> 2- obtain specific funding from a Research Agency (NSF, CNRS?) for par= tly
> formalized PhD fellowships, together with companion funding for the > technical support (eg from the Coq team) to the (partial) formalizatio= n.
>
> 3- obtain good applications, coming from ouside this community.
>
> 4- select the winning applications regarding both the interest of the = naked
> 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 th= ese
> 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 <andrej...@andrej.com>:
>>
>> Apologies for a slightly off topic post, but I think it is relevan= t 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=3D412= 7
>>
>> The conclusion is: it's impossible to make good quality softwa= re in
>> academia because there isn't enough money and because making s= oftware
>> doesn't give one any academic credit.
>>
>> I am afraid formalization of math might fall into the same categor= y,
>> unless we somehow elevate it to a "true science" level. = A great deal
>> has been done in this respect recently by projects lead by Gonthie= r,
>> Hales and Voevodsky, but is it enough? Are we even making a dent?<= br> >>
>> 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 Grundlag= en 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 clas= s
>> when was an undergraduate.
>>
>> With kind regards,
>>
>> Andrej
>>
>> --
>> 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 H= omotopyTypeThe...@googlegroups.com.
>> For more options, visit https://groups.google.com/d/optou= t.
>
>

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTyp= eThe...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--001a113d672c440a2e05351f2895--