How to make software without money

How to make software without money

[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=4127

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

Re: How to make software without money

[Andrej Bauer]

On Sun, Jun 12, 2016 at 10:04 AM, Andrej Bauer <andrej...@andrej.com> wrote:
> http://www.smbc-comics.com/index.php?id=4127

And now for something completely different:
http://wstein.org/talks/2016-06-sage-bp/bp.pdf

Re: [HoTT] How to make software without money

[andré hirschowitz]

[-- Attachment #1: Type: text/plain, Size: 3023 bytes --]

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 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 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 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 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 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 <andrej...@andrej.com>:

> 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=4127
>
> 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.
>

[-- Attachment #2: Type: text/html, Size: 3906 bytes --]

Re: [HoTT] How to make software without money

[Andrej Bauer]

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é 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 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 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 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 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 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 <andrej...@andrej.com>:
>>
>> 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=4127
>>
>> 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.
>
>

RE: [HoTT] How to make software without money

[Joyal, André]

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, 
-André


________________________________________
From: homotopyt...@googlegroups.com [homotopyt...@googlegroups.com] on behalf of Andrej Bauer [andrej...@andrej.com]
Sent: Sunday, June 12, 2016 7:05 AM
To: andré 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é 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 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 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 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 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 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 <andrej...@andrej.com>:
>>
>> 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=4127
>>
>> 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.

Re: [HoTT] How to make software without money

[Ben Sherman]

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 engineer, 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 Consortium, 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 engineers to work on improving the Coq system, and these engineers will prioritize 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 academic institutions can use to pay into the Consortium.)

The goal is that with the Coq Consortium, INRIA researchers will be freed to 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 attention 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 <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 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é 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 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 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 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 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 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 <andrej...@andrej.com>:
>>> 
>>> 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=4127
>>> 
>>> 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.

Re: [HoTT] Re: How to make software without money

[James Cheney]

[-- Attachment #1: Type: text/plain, Size: 3196 bytes --]

Hi Andrej,

This is a problem in many scientific disciplines, not just (formalized)
mathematics.  It is beginning to be understood that software development
and maintenance needs to be recognized as a scholarly activity in order to
make it more likely that software needed to reproduce and understand
research results is available and preserved

https://figshare.com/articles/There_s_No_Such_Thing_As_Irreproducible_Research_Software_Credit_Edition_/3159295/1

and in the UK at least, the Software Sustainability Institute is trying to
support scientists in a range of disciplines to develop better software:

http://software.ac.uk/

Also in the UK, the Alan Turing Institute is supporting "research software
engineers" whose job it will be to turn promising researchware developed by
ATI fellows/students into reusable/documented/tested packages.  So far it
seems that the powers that be view the ATI as primarily about big data and
machine learning, though.  The UK has no analogue to INRIA, nor the US as
far as I know; I think the closest analogues are the national labs but (at
least w.r.t verification and formalized mathematics) they are much less
visible than INRIA.

It would be great to put the problems of formalized mathematics in the
picture for such organizations.

In addition to the recent Coq-related efforts mentioned by others, one
should consider the Isabelle/HOL and ACL2 communities. Isabelle/HOL does
get used in industry, e.g. NICTA/Data61's formalization of sel4 kernel.
See talks by J Moore on ACL2 and by Gerwin Klein on sel4 at the recent
Royal Society discussion meeting on "verified trustworthy software systems"

https://royalsociety.org/events/2016/04/software-systems/

There are also (relative) success stories in mathematics, e.g. the GAP
system:

www.gap-system.org/

None of this is to say that software credit and maintenance (and
development to the level of maturity needed for acceptance in the
mathematical community) is a solved problem, but there are other solution
attempts that can be considered to better understand the problem.
Fundamentally, what is needed is resources, whether this means money from
funding agencies, investment capital, or donations of free time from open
source contributors. In each case, persuasion and leadership is needed, but
what form this takes seems very situation-dependent and there is no
guarantee that the needed model will fit anyone's pre-existing vision of a
"successful [academic] career".

--James

PS. I also enjoyed the comic.


On Sun, Jun 12, 2016 at 9:28 AM, Andrej Bauer <andrej...@andrej.com>
wrote:

> On Sun, Jun 12, 2016 at 10:04 AM, Andrej Bauer <andrej...@andrej.com>
> wrote:
> > http://www.smbc-comics.com/index.php?id=4127
>
> And now for something completely different:
> http://wstein.org/talks/2016-06-sage-bp/bp.pdf
>
> --
> 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.
>

[-- Attachment #2: Type: text/html, Size: 4399 bytes --]

Re: [HoTT] How to make software without money

[Timothy Carstens]

[-- Attachment #1: Type: text/plain, Size: 6766 bytes --]

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 <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 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é 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 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
> 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 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
> 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 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 <andrej...@andrej.com>:
> >>
> >> 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=4127
> >>
> >> 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.
>

[-- Attachment #2: Type: text/html, Size: 8362 bytes --]

Re: [HoTT] How to make software without money

[Vladimir Voevodsky]

[-- Attachment #1.1: Type: text/plain, Size: 5610 bytes --]

I think the key step that needs to be done is to start to teach mathematics using proof assistants similarly to how the Software Foundation initiative does it for programming languages.

It may be at first a graduate course in constructive mathematics e.g. in constructive algebra.

Due to the way the motivational structure of mathematical learning is organized it would be very good and may even be necessary for such a course to succeed to have several unsolved *conjectures* or *problems* to attract students.

I know of one such problem - to find a constructive proof of Merkurjev-Suslin theorem about K_2/l . Constructive here might mean simply a proof that does not use the axiom of choice but I believe that to find such a proof one has to learn real constructive algebra such as the constructive description of the algebraic closure of a field (one can assume that it has decidable equality).

I also believe that finding a constructive proof pf this theorem will open the way to the correct formulation and proofs of many questions related to the structure of Galois cohomology that we at the moment have no idea how to approach.

I have a feeling that there are also many such questions in number theory where having a constructive proof would mean achieving a much higher level of understanding of the structures involved and ultimately to the solutions of problems that are open in classical mathematics.

Vladimir.






> On Jun 12, 2016, at 4:20 PM, James Cheney <james....@gmail.com> wrote:
> 
> Hi Andrej,
> 
> This is a problem in many scientific disciplines, not just (formalized) mathematics.  It is beginning to be understood that software development and maintenance needs to be recognized as a scholarly activity in order to make it more likely that software needed to reproduce and understand research results is available and preserved
> 
> https://figshare.com/articles/There_s_No_Such_Thing_As_Irreproducible_Research_Software_Credit_Edition_/3159295/1 <https://figshare.com/articles/There_s_No_Such_Thing_As_Irreproducible_Research_Software_Credit_Edition_/3159295/1>
> 
> and in the UK at least, the Software Sustainability Institute is trying to support scientists in a range of disciplines to develop better software:
> 
> http://software.ac.uk/ <http://software.ac.uk/>
> 
> Also in the UK, the Alan Turing Institute is supporting "research software engineers" whose job it will be to turn promising researchware developed by ATI fellows/students into reusable/documented/tested packages.  So far it seems that the powers that be view the ATI as primarily about big data and machine learning, though.  The UK has no analogue to INRIA, nor the US as far as I know; I think the closest analogues are the national labs but (at least w.r.t verification and formalized mathematics) they are much less visible than INRIA.
> 
> It would be great to put the problems of formalized mathematics in the picture for such organizations.
> 
> In addition to the recent Coq-related efforts mentioned by others, one should consider the Isabelle/HOL and ACL2 communities. Isabelle/HOL does get used in industry, e.g. NICTA/Data61's formalization of sel4 kernel.  See talks by J Moore on ACL2 and by Gerwin Klein on sel4 at the recent Royal Society discussion meeting on "verified trustworthy software systems"
> 
> https://royalsociety.org/events/2016/04/software-systems/ <https://royalsociety.org/events/2016/04/software-systems/>
> 
> There are also (relative) success stories in mathematics, e.g. the GAP system:
> 
> www.gap-system.org/ <http://www.gap-system.org/>
> 
> None of this is to say that software credit and maintenance (and development to the level of maturity needed for acceptance in the mathematical community) is a solved problem, but there are other solution attempts that can be considered to better understand the problem.  Fundamentally, what is needed is resources, whether this means money from funding agencies, investment capital, or donations of free time from open source contributors. In each case, persuasion and leadership is needed, but what form this takes seems very situation-dependent and there is no guarantee that the needed model will fit anyone's pre-existing vision of a "successful [academic] career".
> 
> --James
> 
> PS. I also enjoyed the comic.
> 
> 
> On Sun, Jun 12, 2016 at 9:28 AM, Andrej Bauer <andrej...@andrej.com <mailto:andrej...@andrej.com>> wrote:
> On Sun, Jun 12, 2016 at 10:04 AM, Andrej Bauer <andrej...@andrej.com <mailto:andrej...@andrej.com>> wrote:
> > http://www.smbc-comics.com/index.php?id=4127 <http://www.smbc-comics.com/index.php?id=4127>
> 
> And now for something completely different:
> http://wstein.org/talks/2016-06-sage-bp/bp.pdf <http://wstein.org/talks/2016-06-sage-bp/bp.pdf>
> 
> --
> 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 <mailto:HomotopyTypeTheo...@googlegroups.com>.
> For more options, visit https://groups.google.com/d/optout <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 <mailto:HomotopyTypeThe...@googlegroups.com>.
> For more options, visit https://groups.google.com/d/optout <https://groups.google.com/d/optout>.


[-- Attachment #1.2: Type: text/html, Size: 7894 bytes --]

[-- Attachment #2: Message signed with OpenPGP using GPGMail --]
[-- Type: application/pgp-signature, Size: 507 bytes --]

Re: [HoTT] How to make software without money

[Bas Spitters]

Regarding proof assistants in teaching, let me mention the very nice
work by Jeremy Avigad:
   https://avigad.github.io/logic_and_proof/



On Mon, Jun 13, 2016 at 2:00 PM, Vladimir Voevodsky <vlad...@ias.edu> wrote:
> I think the key step that needs to be done is to start to teach mathematics
> using proof assistants similarly to how the Software Foundation initiative
> does it for programming languages.
>
> It may be at first a graduate course in constructive mathematics e.g. in
> constructive algebra.
>
> Due to the way the motivational structure of mathematical learning is
> organized it would be very good and may even be necessary for such a course
> to succeed to have several unsolved *conjectures* or *problems* to attract
> students.
>
> I know of one such problem - to find a constructive proof of
> Merkurjev-Suslin theorem about K_2/l . Constructive here might mean simply a
> proof that does not use the axiom of choice but I believe that to find such
> a proof one has to learn real constructive algebra such as the constructive
> description of the algebraic closure of a field (one can assume that it has
> decidable equality).
>
> I also believe that finding a constructive proof pf this theorem will open
> the way to the correct formulation and proofs of many questions related to
> the structure of Galois cohomology that we at the moment have no idea how to
> approach.
>
> I have a feeling that there are also many such questions in number theory
> where having a constructive proof would mean achieving a much higher level
> of understanding of the structures involved and ultimately to the solutions
> of problems that are open in classical mathematics.
>
> Vladimir.
>
>
>
>
>
>
> On Jun 12, 2016, at 4:20 PM, James Cheney <james....@gmail.com> wrote:
>
> Hi Andrej,
>
> This is a problem in many scientific disciplines, not just (formalized)
> mathematics.  It is beginning to be understood that software development and
> maintenance needs to be recognized as a scholarly activity in order to make
> it more likely that software needed to reproduce and understand research
> results is available and preserved
>
> https://figshare.com/articles/There_s_No_Such_Thing_As_Irreproducible_Research_Software_Credit_Edition_/3159295/1
>
> and in the UK at least, the Software Sustainability Institute is trying to
> support scientists in a range of disciplines to develop better software:
>
> http://software.ac.uk/
>
> Also in the UK, the Alan Turing Institute is supporting "research software
> engineers" whose job it will be to turn promising researchware developed by
> ATI fellows/students into reusable/documented/tested packages.  So far it
> seems that the powers that be view the ATI as primarily about big data and
> machine learning, though.  The UK has no analogue to INRIA, nor the US as
> far as I know; I think the closest analogues are the national labs but (at
> least w.r.t verification and formalized mathematics) they are much less
> visible than INRIA.
>
> It would be great to put the problems of formalized mathematics in the
> picture for such organizations.
>
> In addition to the recent Coq-related efforts mentioned by others, one
> should consider the Isabelle/HOL and ACL2 communities. Isabelle/HOL does get
> used in industry, e.g. NICTA/Data61's formalization of sel4 kernel.  See
> talks by J Moore on ACL2 and by Gerwin Klein on sel4 at the recent Royal
> Society discussion meeting on "verified trustworthy software systems"
>
> https://royalsociety.org/events/2016/04/software-systems/
>
> There are also (relative) success stories in mathematics, e.g. the GAP
> system:
>
> www.gap-system.org/
>
> None of this is to say that software credit and maintenance (and development
> to the level of maturity needed for acceptance in the mathematical
> community) is a solved problem, but there are other solution attempts that
> can be considered to better understand the problem.  Fundamentally, what is
> needed is resources, whether this means money from funding agencies,
> investment capital, or donations of free time from open source contributors.
> In each case, persuasion and leadership is needed, but what form this takes
> seems very situation-dependent and there is no guarantee that the needed
> model will fit anyone's pre-existing vision of a "successful [academic]
> career".
>
> --James
>
> PS. I also enjoyed the comic.
>
>
> On Sun, Jun 12, 2016 at 9:28 AM, Andrej Bauer <andrej...@andrej.com>
> wrote:
>>
>> On Sun, Jun 12, 2016 at 10:04 AM, Andrej Bauer <andrej...@andrej.com>
>> wrote:
>> > http://www.smbc-comics.com/index.php?id=4127
>>
>> And now for something completely different:
>> http://wstein.org/talks/2016-06-sage-bp/bp.pdf
>>
>> --
>> 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.
>
>
> --
> 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.