From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-0.9 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-qk1-x73c.google.com (mail-qk1-x73c.google.com [IPv6:2607:f8b0:4864:20::73c]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 02801f14 for ; Sun, 3 Nov 2019 11:38:51 +0000 (UTC) Received: by mail-qk1-x73c.google.com with SMTP id a16sf3130435qka.10 for ; Sun, 03 Nov 2019 03:38:50 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1572781130; cv=pass; d=google.com; s=arc-20160816; b=KGrHRrfMfPtV6i8g9Mxr9hIGLjoeUHs0fRQp57TZ/sw3hmjJGVZGqwXxN61ERE70Vm n7MFxn15KdIpIUVcVUyxGpPU+gclgkfnJsAQmR9wYdEsnEj1ce1iazc9DxS0eBnZx/Ru vhphjVDWEoNPSuGUGBN+HZPVQBPf7UeobByO6h8nbZshonIMzN8JiZVH/+hkGif7VBvV bTbQPedl32BO0bdowjW4hvcwgOqdoSFk1e1A2A92wheeoYvKBlfVM+66mSvA6zrADOB9 +fDxJ8Jf5SsvV/MDbynLPiKrxfCp4HhNogFf1AMVQrCmMYp9A80bZ2eZ1F0VqRy3C4So HG/w== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:sender:dkim-signature :dkim-signature; bh=tVqF/mJXnUWFXCFmkoQBg4ji/xf5amVYIdmGvwzAv/8=; b=uHdgdU31XV/namZROT0niZCT/gGTiDubg6I83zHJY2xeSLE8LMjElsx1OJqWJgnbrm qtJ5YiLffDh9yPaA7iUf3JprwGNUu0OBlZiR8frs5w+Y7WSZT+X9XXDTQVOn3h8xQRZM Af6znE6oTAMyrDWoiPplq5tbucHJAQXVxuMYaihjFZzkWqkQXJ0iHFTwqXroR6Bk5mbV mBWyfRPX+N2GWlPyH8R/3QldzwojRkhUYMmhHhSqBO+liQC1VUij/Li6pfwDvs2qQ/FM jhWRatCDB7ZpJdoEiJrKolcXu6jj/HgCljxp0+iPTxKYw9+0uN7s/e9UKQcLo6LjXMLi 3SWw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=CMORUJs7; spf=pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::b2d as permitted sender) smtp.mailfrom=b.a.w.spitters@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:references:in-reply-to:from:date:message-id :subject:to:cc:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=tVqF/mJXnUWFXCFmkoQBg4ji/xf5amVYIdmGvwzAv/8=; b=hyQ6nhMZPtwBWVqoxcvxHRtVOXYXZV74O0ksJLk++f2ngNEK1dYfBxt9B+ez3pNisa auPW3D00D9ihMjec2ohIrVY6oVSK0yeQDksJvUCg4FXgVVMw2GMyTS9ODz3/G3oVY7wJ uLSSXRTP9Die+ywTEcSWks4hswQjOW9glCGtN0KvcL8BkdaYTkdvjK3sHumf96kJTycu PBI4xMWBUo/MKLrteqDhH5Szmvo2hCOU4FUW6jl6NXmDq/R7eQms2jeQ8Ds/kDkXJ1AG fJSTLjhbIB5AytO3j/z21lhmnUDlokZyWwH6mrzGJTAQQsA+ZQRW82SIRfm24/VqaqJs Y0Lg== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc:x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=tVqF/mJXnUWFXCFmkoQBg4ji/xf5amVYIdmGvwzAv/8=; b=tPXln7bVSgzOqqyP7YEWXRlMGKRLFAcM+qJ016zp0CLady2eE4T+HMTFYvnYRRTcl3 jfwbOMJc3NIHRk+XtIcNRXcKNX8brpC3ahoKpi9o04XJxCe1IE2QQzVNJGE0CO2KUHY+ TggaKyj5O6DBMAB/LFopjmvnLB8BOk6UpQeZztqtoKXil6BlGjY7vfyXHjtYSxVXTzM7 R2W5QcqZkxvL5PkWVu2PUXdaemMWYa85bHqT/Ey+I99iOU1WZIJ4x/rN13NXBq/RxcdD 5bjhopYyTuNMIIopKEOUd2QLtSbS3WTa210WNw9aXnUtN0GkgAkfiDAtvhuvSfbZWnkS L8og== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:references:in-reply-to:from :date:message-id:subject:to:cc:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :x-spam-checked-in-group:list-post:list-help:list-archive :list-unsubscribe; bh=tVqF/mJXnUWFXCFmkoQBg4ji/xf5amVYIdmGvwzAv/8=; b=anMy3A7wMZZYaZhJacA4yY8orxgd5gNiTGhaVUnpf/1kQlN/enYb/pIUTjF4LstfvK TD5cJLafdZlzMDQQHRcTe8I1cVcZkmySbnP3Okz4N5xE/duZS+QEN2PvQlyi3GzTGD+B kn1Z8yC44Mxkzv/5eAhp7lNQXCcy0ZuwUosrFc8acyVL1L+P1qdyKIzqOwXq3zTCQ+WK 39LKg5XToaqPOrWEnwwDif/lbGsI0zBQ5KZiR6Y0XP1bmf6LVX06+5N+gRJ0ESd0TeOz FhYroDn69r0p1kpG1pmGuTHX9O4bhG65Vg+pLCLXZy8xwpMrEFHXWuu2JKI1FNLaaj+X FIeA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAWVRhXgGDZzg24qB8RdbPuE4p8dSf5PFm7dOZzBu4+ysDgnUf1N oUJOqyg8BuD+jnYcBNWhWHY= X-Google-Smtp-Source: APXvYqyZflaO+kfogHrrebMpFBo2VHOneUHHEiS0buGcdaMl7/wZkS/Pjd2NJPnD5+h0yuMP+0pKUA== X-Received: by 2002:a05:620a:704:: with SMTP id 4mr5272168qkc.177.1572781128764; Sun, 03 Nov 2019 03:38:48 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:6214:13b4:: with SMTP id h20ls994586qvz.0.gmail; Sun, 03 Nov 2019 03:38:48 -0800 (PST) X-Received: by 2002:a05:6214:8c6:: with SMTP id da6mr18317675qvb.1.1572781128275; Sun, 03 Nov 2019 03:38:48 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1572781128; cv=none; d=google.com; s=arc-20160816; b=wFFiOCdk5x6B5crVQYipXC/FINf3dAf5GWGka+ScY8UZx1DSJO8sm9vHtOWGzkxR/2 nm9Zn0hFVWNexpyLkmdlBCeJWAuuowszbefoLhpj1OT9L1oRUitm6YSylWkxdMTcvUh9 uN6rxi5+yYfR4XAFRCL/IWnUeKWURlyx8NyXn2KSSjeWs5ltfgBKtHHtQdKXJMEaUiiB TPejhOU8fhHAPXtNOVmX14k0z5DvsHAytXe+UaEZ8lLM5ZYC705l/i8eeILT/sZVnrVP A4VJWRe3bjK/cGIi0ITGOEg1qq+KOR2Jw8PkIfz5Cxf2y9Eq7+wxxdLzZ1OVcXDZy8Ra bQDw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:dkim-signature; bh=82d+TjcUH8/PwezFBuur6wqgmMm8BXSdJaW+qJiqqGA=; b=nu1vcRxErYC/D1hrJCYl+bsvmtuNWCfrIiQsV8lFtMemFI550HbjSMozQPJNmB/bRo g34+GW0mbgXjPQY0/vmOPpGjVh9z3h+QdcazaMTmRuvQKgKMpQb8MyX2yZZPL4UPQjjF w3Kc19WLqLHAvicIjxsky20lMuEXi1Th3dvFx0PVbgoH3x9bWG7/Ptq19zcL2HNlTE9i To3wTvC/RL3oHBIOvxE1aW634iQ1Xjj3aI42cner+qvj3uw/aln+oi4t9QBy5ENkTPP8 +XsR209qH3QbA98gFJrShMcwySXLJ7v103MpwoOZq0D7W9caEhhFtmMmDL4BxvfH62jF m7rw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=CMORUJs7; spf=pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::b2d as permitted sender) smtp.mailfrom=b.a.w.spitters@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-yb1-xb2d.google.com (mail-yb1-xb2d.google.com. [2607:f8b0:4864:20::b2d]) by gmr-mx.google.com with ESMTPS id k33si722820qtd.4.2019.11.03.03.38.48 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sun, 03 Nov 2019 03:38:48 -0800 (PST) Received-SPF: pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::b2d as permitted sender) client-ip=2607:f8b0:4864:20::b2d; Received: by mail-yb1-xb2d.google.com with SMTP id e14so6609860ybk.0 for ; Sun, 03 Nov 2019 03:38:48 -0800 (PST) X-Received: by 2002:a25:bbce:: with SMTP id c14mr18406437ybk.447.1572781127753; Sun, 03 Nov 2019 03:38:47 -0800 (PST) MIME-Version: 1.0 References: In-Reply-To: From: Bas Spitters Date: Sun, 3 Nov 2019 12:38:36 +0100 Message-ID: Subject: Re: [HoTT] Why did Voevodsky find existing proof assistants to be 'impractical'? To: Nicolas Alexander Schmidt Cc: Homotopy Type Theory Content-Type: multipart/alternative; boundary="0000000000006de65605966fa444" X-Original-Sender: b.a.w.spitters@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=CMORUJs7; spf=pass (google.com: domain of b.a.w.spitters@gmail.com designates 2607:f8b0:4864:20::b2d as permitted sender) smtp.mailfrom=b.a.w.spitters@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , --0000000000006de65605966fa444 Content-Type: text/plain; charset="UTF-8" There's also VV homotopy lambda calculus, which he later abandoned for MLTT: https://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/Hlambda_short_current.pdf On Sun, Oct 27, 2019 at 6:22 PM Bas Spitters wrote: > I believe it refers to his 2-theories: > https://www.ias.edu/ideas/2014/voevodsky-origins > > On Sun, Oct 27, 2019 at 3:41 PM Nicolas Alexander Schmidt < > zero@fromzerotoinfinity.xyz> wrote: > >> In [this](https://www.youtube.com/watch?v=zw6NcwME7yI&t=1680) 2014 talk >> at IAS, Voevodsky talks about the history of his project of "univalent >> mathematics" and his motivation for starting it. Namely, he mentions >> that he found existing proof assistants at that time (in 2000) to be >> impractical for the kinds of mathematics he was interested in. >> >> Unfortunately, he doesn't go into details of what mathematics he was >> exactly interested in (I'm guessing something to do with homotopy >> theory) or why exactly existing proof assistants weren't practical for >> formalizing them. Judging by the things he mentions in his talk, it >> seems that (roughly) his rejection of those proof assistants was based >> on the view that predicate logic + ZFC is not expressive enough. In >> other words, there is too much lossy encoding needed in order to >> translate from the platonic world of mathematical ideas to this formal >> language. >> >> Comparing the situation to computer programming languages, one might say >> that predicate logic is like Assembly in that even though everything can >> be encoded in that language, it is not expressive enough to directly >> talk about higher level concepts, diminishing its practical value for >> reasoning about mathematics. In particular, those systems are not >> adequate for *interactive* development of *new* mathematics (as opposed >> to formalization of existing theories). >> >> Perhaps I am just misinterpreting what Voevodsky said. In this case, I >> hope someone can correct me. However even if this wasn't *his* view, to >> me it seems to be a view held implicitly in the HoTT community. In any >> case, it's a view that one might reasonably hold. >> >> However I wonder how reasonable that view actually is, i.e. whether e.g. >> Mizar really is that much more impractical than HoTT-Coq or Agda, given >> that people have been happily formalizing mathematics in it for 46 years >> now. And, even though by browsing the contents of "Formalized >> Mathematics" one can get the impression that the work consists mostly of >> formalizing early 20th century mathematics, neither the UniMath nor the >> HoTT library for example contain a proof of Fubini's theorem. >> >> So, to put this into one concrete question, how (if at all) is HoTT-Coq >> more practical than Mizar for the purpose of formalizing mathematics, >> outside the specific realm of synthetic homotopy theory? >> >> >> -- >> >> Nicolas >> >> >> -- >> 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. >> To view this discussion on the web visit >> https://groups.google.com/d/msgid/HomotopyTypeTheory/e491d38b-b50a-6172-dca9-40d45fe1b6d2%40fromzerotoinfinity.xyz >> . >> > -- 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOoPQuRQPMkCFKYtAbB%2BpNK90XtFk%2BaVT_aY59U_-9t17sBzeA%40mail.gmail.com. --0000000000006de65605966fa444 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
There's also VV homotopy lambda calculus, which h= e later abandoned for MLTT:

On Sun, Oct 27, 2019 at 6:22 PM Bas Spitters <b.a.w.spitters@gmail.com> = wrote:
I believe it refers to his 2-theories:

On Sun, Oct 27, 2019= at 3:41 PM Nicolas Alexander Schmidt <zero@fromzerotoinfinity.xyz> wrote:<= br>
In [this](https://www.youtube.com/watch?v=3Dzw6NcwME7yI&am= p;t=3D1680) 2014 talk
at IAS, Voevodsky talks about the history of his project of "univalent=
mathematics" and his motivation for starting it. Namely, he mentions that he found existing proof assistants at that time (in 2000) to be
impractical for the kinds of mathematics he was interested in.

Unfortunately, he doesn't go into details of what mathematics he was exactly interested in (I'm guessing something to do with homotopy
theory) or why exactly existing proof assistants weren't practical for<= br> formalizing them. Judging by the things he mentions in his talk, it
seems that (roughly) his rejection of those proof assistants was based
on the view that predicate logic + ZFC is not expressive enough. In
other words, there is too much lossy encoding needed in order to
translate from the platonic world of mathematical ideas to this formal
language.

Comparing the situation to computer programming languages, one might say that predicate logic is like Assembly in that even though everything can be encoded in that language, it is not expressive enough to directly
talk about higher level concepts, diminishing its practical value for
reasoning about mathematics. In particular, those systems are not
adequate for *interactive* development of *new* mathematics (as opposed
to formalization of existing theories).

Perhaps I am just misinterpreting what Voevodsky said. In this case, I
hope someone can correct me. However even if this wasn't *his* view, to=
me it seems to be a view held implicitly in the HoTT community. In any
case, it's a view that one might reasonably hold.

However I wonder how reasonable that view actually is, i.e. whether e.g. Mizar really is that much more impractical than HoTT-Coq or Agda, given
that people have been happily formalizing mathematics in it for 46 years now. And, even though by browsing the contents of "Formalized
Mathematics" one can get the impression that the work consists mostly = of
formalizing early 20th century mathematics, neither the UniMath nor the
HoTT library for example contain a proof of Fubini's theorem.

So, to put this into one concrete question, how (if at all) is HoTT-Coq
more practical than Mizar for the purpose of formalizing mathematics,
outside the specific realm of synthetic homotopy theory?


--

Nicolas


--
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 HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.googl= e.com/d/msgid/HomotopyTypeTheory/e491d38b-b50a-6172-dca9-40d45fe1b6d2%40fro= mzerotoinfinity.xyz.

--
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 = HomotopyTypeTheory+unsubscribe@googlegroups.com.
To view this discussion on the web visit https:/= /groups.google.com/d/msgid/HomotopyTypeTheory/CAOoPQuRQPMkCFKYtAbB%2BpNK90X= tFk%2BaVT_aY59U_-9t17sBzeA%40mail.gmail.com.
--0000000000006de65605966fa444--