From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.io!.POSTED.blaine.gmane.org!not-for-mail From: Emanuel Berg via Users list for the GNU Emacs text editor Newsgroups: gmane.emacs.help Subject: Re: [OFFTOPIC] Re: Appending lists Date: Sat, 19 Jun 2021 02:04:26 +0200 Message-ID: <87im2a3ek5.fsf@zoho.eu> References: <4tl1yvylvg1fxx5eefjs9mnk.1623688568572@email.android.com> <87o8c8l32h.fsf@posteo.net> <87zgvs2bup.fsf@zoho.eu> <87y2bby1kr.fsf@zoho.eu> <20210615091834.GB24886@tuxteam.de> <87im2ewr3k.fsf@zoho.eu> <20210616072819.GB17919@tuxteam.de> <20210616151101.GB5669@tuxteam.de> <875yydtnqz.fsf@zoho.eu> Reply-To: Emanuel Berg Mime-Version: 1.0 Content-Type: text/plain Injection-Info: ciao.gmane.io; posting-host="blaine.gmane.org:116.202.254.214"; logging-data="37618"; mail-complaints-to="usenet@ciao.gmane.io" User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/28.0.50 (gnu/linux) To: help-gnu-emacs@gnu.org Cancel-Lock: sha1:yVMnqICTkIBe+8BBO4rpOiW+Lc0= Original-X-From: help-gnu-emacs-bounces+geh-help-gnu-emacs=m.gmane-mx.org@gnu.org Sat Jun 19 02:06:05 2021 Return-path: Envelope-to: geh-help-gnu-emacs@m.gmane-mx.org Original-Received: from lists.gnu.org ([209.51.188.17]) by ciao.gmane.io with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.92) (envelope-from ) id 1luOUu-0009bL-PW for geh-help-gnu-emacs@m.gmane-mx.org; Sat, 19 Jun 2021 02:06:04 +0200 Original-Received: from localhost ([::1]:50842 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1luOUt-0003a5-Fc for geh-help-gnu-emacs@m.gmane-mx.org; Fri, 18 Jun 2021 20:06:03 -0400 Original-Received: from eggs.gnu.org ([2001:470:142:3::10]:41552) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1luOTx-0003Zw-3m for help-gnu-emacs@gnu.org; Fri, 18 Jun 2021 20:05:05 -0400 Original-Received: from ciao.gmane.io ([116.202.254.214]:59594) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1luOTu-00010a-W3 for help-gnu-emacs@gnu.org; Fri, 18 Jun 2021 20:05:04 -0400 Original-Received: from list by ciao.gmane.io with local (Exim 4.92) (envelope-from ) id 1luOTt-0008EB-L2 for help-gnu-emacs@gnu.org; Sat, 19 Jun 2021 02:05:01 +0200 X-Injected-Via-Gmane: http://gmane.org/ Mail-Followup-To: help-gnu-emacs@gnu.org Mail-Copies-To: never Received-SPF: pass client-ip=116.202.254.214; envelope-from=geh-help-gnu-emacs@m.gmane-mx.org; helo=ciao.gmane.io X-Spam_score_int: -16 X-Spam_score: -1.7 X-Spam_bar: - X-Spam_report: (-1.7 / 5.0 requ) BAYES_00=-1.9, HEADER_FROM_DIFFERENT_DOMAINS=0.249, SPF_HELO_NONE=0.001, SPF_PASS=-0.001 autolearn=no autolearn_force=no X-Spam_action: no action X-BeenThere: help-gnu-emacs@gnu.org X-Mailman-Version: 2.1.23 Precedence: list List-Id: Users list for the GNU Emacs text editor List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: help-gnu-emacs-bounces+geh-help-gnu-emacs=m.gmane-mx.org@gnu.org Original-Sender: "help-gnu-emacs" Xref: news.gmane.io gmane.emacs.help:131001 Archived-At: Stefan Monnier wrote: > https://www.quantamagazine.org/does-time-really-flow-new-clues-come-from-a-century-old-approach-to-math-20200407/ > > [ The relationship being that type theory is generally > associated with constructive logic rather than with > classical logic. ] Eh, "type theory"? Are we talking types like in a programming language? There is a theory behind that? I always thought it was just a matter of arranging 0s and 1 in a way that was agreed-upon locally to denote that something is something so it can be recognized and operated upon/used in certain ways? Much like a network communication protocol. Like question one, what does the messages look like (how are they organized)? Question two, in what order are they supposed to come? Question three, what does it all mean? And that's it? Well, maybe there is a theory to networks as well, now that I think about it. Of course there is. Bad example. But that still feels more theoretic than types, with node diagrams and stuff... -- underground experts united https://dataswamp.org/~incal