Re: [HoTT] How to make software without money

[Bas Spitters <b.a.w.s...@gmail.com>]

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.