Re: [HoTT] Re: Where is the problem with initiality?

[Richard Williamson <rwilli...@gmail.com>]

Alexander is getting a fair bit of stick! I just wanted to add a
note of support to one aspect of the point I think he is making:
there is a reason that languages such as Python are widely used
by perfectly competent programmers who fully understand the
benefits of typing.

I share the view that there has to be something rather more
Python-like in syntax than the currently available syntaxes if
one is to have any hope of having something usable in practise by
people who just want to get on with the mathematics. I am not
convinced that this is a purely engineering problem as opposed to
a theoretical one.

(Yes, Python is not untyped either, but I think the point
stands).

On Tue, Jun 05, 2018 at 09:52:26AM +0200, Andrej Bauer wrote:
> Dear Alexander,
>
>
> On Wed, May 30, 2018 at 12:53 PM, Alexander Kurz <axh...@gmail.com> wrote:
> >
> > It is crucial that informal mathematics is untyped. The untypedness is what makes it flexible enough for practical purposes. Formalising mathematics in a proof assistant is hard work. And to a large extent this is due to the fact that everything has to be typed.
> >
> > If we ever want to get mathematicians to use proof assistants as casually as they use latex, the problem of untyped vs typed mathematics needs to be solved.
>
> I think you made there a coiple of intellectual jumps. In order for
> your statements to have some weight, you need to consider the
> following questions:
>
> (a) What if formalization of mathematics in existing proof assistants
> is hard for some reason other than typedness?
>
> (b) Most proof assistants that have a large user base are typed. Is
> this is a big conspiracy on part of the designers, or could it be
> understood as evidence that typed proof assistants have a certain
> advantage over the untyped ones?
>
> (c) You offer LaTeX as an example of good design. I beg to differ.
>
> (d) Informal mathematics is very obviously typed, as witnessed by the
> fact that authors are always carefully explain the types of various
> symbols they use (or rely on the culturally accepted notations).
>
> The Buffon needle example presents absolutely no obstacle to typing.
> Perhaps you are mixing up *informal* nature of human mathematics with
> untypedness? Formalizing Buffon's needle requires a great amount of
> precision (what is a curve? what does it mean to "throw a needle"? how
> do we cuunt crossings when there are infinitely many?) which is
> unavoidable so long as we subbscribe to the mathematical method.
> Typedness has nothing to do with this fact.
>
> 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.