220 40916 <987a5677-b6fd-46d0-8655-6e5c582a136a@isocpp.org> article
Path: news.gmane.org!.POSTED!not-for-mail
From: FrankHB1989 <frankhb1989@gmail.com>
Newsgroups: gmane.comp.lang.c++.isocpp.proposals
Subject: Re: Re: please discontinue the command of the [while]
 and [do,while]
Date: Wed, 7 Nov 2018 21:17:28 -0800 (PST)
Lines: 117
Approved: news@gmane.org
Message-ID: <987a5677-b6fd-46d0-8655-6e5c582a136a@isocpp.org>
References: <8c5cefbc-3565-4add-ae37-37d730e853c9@isocpp.org>
 <pruqva$lnu$1@blaine.gmane.org> <0c89963c-d5e4-49f2-a460-fb987ec5a50a@isocpp.org>
 <CAOU91ONMjey1H8bznGzAWCkCfEutatKXdmm0sa+C5H8=J4q3bQ@mail.gmail.com> <94ffcfd5-0657-4632-95d9-efc88208a8d6@isocpp.org>
 <CA+EzHGdvL2k3CS+oeC7e8fmviEVj7PD2OLQiBEJLTf2QZMqUWA@mail.gmail.com>
Reply-To: std-proposals@isocpp.org
NNTP-Posting-Host: blaine.gmane.org
Mime-Version: 1.0
Content-Type: multipart/mixed; 
	boundary="----=_Part_264_1437820450.1541654248247"
X-Trace: blaine.gmane.org 1541654126 16981 195.159.176.226 (8 Nov 2018 05:15:26 GMT)
X-Complaints-To: usenet@blaine.gmane.org
NNTP-Posting-Date: Thu, 8 Nov 2018 05:15:26 +0000 (UTC)
To: ISO C++ Standard - Future Proposals <std-proposals@isocpp.org>
Original-X-From: std-proposals+bncBCTJVBPG3QIBB2MNR7PQKGQE6WHKOMA@isocpp.org Thu Nov 08 06:15:22 2018
Return-path: <std-proposals+bncBCTJVBPG3QIBB2MNR7PQKGQE6WHKOMA@isocpp.org>
Envelope-to: gclcip-std-proposals@m.gmane.org
Original-Received: from mail-yb1-f198.google.com ([209.85.219.198])
	by blaine.gmane.org with esmtp (Exim 4.84_2)
	(envelope-from <std-proposals+bncBCTJVBPG3QIBB2MNR7PQKGQE6WHKOMA@isocpp.org>)
	id 1gKcf2-0004HW-Au
	for gclcip-std-proposals@m.gmane.org; Thu, 08 Nov 2018 06:15:20 +0100
Original-Received: by mail-yb1-f198.google.com with SMTP id f83-v6sf14368403ybg.8
        for <gclcip-std-proposals@m.gmane.org>; Wed, 07 Nov 2018 21:17:30 -0800 (PST)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
        d=isocpp-org.20150623.gappssmtp.com; s=20150623;
        h=date:from:to:message-id:in-reply-to:references:subject:mime-version
         :x-original-sender:reply-to:precedence:mailing-list:list-id
         :list-post:list-help:list-archive:list-subscribe:list-unsubscribe;
        bh=17thKds0p637YlhdyhNubu6XCdelET2NqXPk384RKJ4=;
        b=Lxc1zTGUVmjTYxTf3bVkhKeYzFzcsgf7tF6sLBhfG74uOthwjDH/0y7bLS1MptkgWL
         OtpmTOw2guZ+O+TkYZntcGrUfA8Xf4R/PTyZrGrIY0TpuSt/qlLtnz/EpCBzJooUVKXb
         xvzQ2jrK+n7UsCnIcpMxVLPZr++mwU4ZEwqLKiCtJEJJG2aJJY6fR5rE6ncuInuN/ES+
         iXkEloFuE3O/fZVERcz8YID1XMGvE1ffNLTfRACFT1cbVAzQ8igo1GQwTaWjh2mYsO3j
         81DIICJNPvnVfjBMISHBa5bZJX+tRNleDKuZQEc6G+5Hm0cgebnWtSDwu0uDEFbnxfrY
         D/kQ==
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
        d=gmail.com; s=20161025;
        h=date:from:to:message-id:in-reply-to:references:subject:mime-version
         :x-original-sender:reply-to:precedence:mailing-list:list-id
         :list-post:list-help:list-archive:list-subscribe:list-unsubscribe;
        bh=17thKds0p637YlhdyhNubu6XCdelET2NqXPk384RKJ4=;
        b=ushnOwbS3N9SEuQ6/L4Mc2KLDvfXXTcG9Pz1W4w5dkjJ6BQnI0UUSvok/PUpwFojmB
         nNf8QsPesK9i67ahKMELuQB8eCYsSKLCTlQf9yxwGZRXVFuy7NPMvLZTZyiCyUbivVeO
         ikDpMLEJE4HWLoqS5opu1+cv+z5ee/qhJ4ueViJiRKO55l8YYrZIqFqW8NFWypTDygXh
         k3xBF0E4hBCUIPGo39ETR0qWfdccsGPKsBtoUp8yzQpgL7XbLy01vKVfmRJ46o6Ddevu
         usPdaRZro2cuYEO94urv8NgfhRnpuZR01QC3Wcj/7AllT20K+4KbTmhNBgKzjuD3lC6D
         r1+Q==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
        d=1e100.net; s=20161025;
        h=x-gm-message-state:date:from:to:message-id:in-reply-to:references
         :subject:mime-version:x-original-sender:reply-to:precedence
         :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help
         :list-archive:list-subscribe:list-unsubscribe;
        bh=17thKds0p637YlhdyhNubu6XCdelET2NqXPk384RKJ4=;
        b=UyjLK+QU/QzN5ziXWp0Zc9HQErfSanLwVjzrfTO5fv2yVqoTOsAa5L1JLCUwEp+U/8
         JkMmR21X+0ppZFjuIc9aOFJ4yYePk/CpDj4iMAVq/ouvqvQzBf0HVcZI5mgryi/CZAwo
         aOsCSO1w8f1KFlWpToalnl21Nub26F9Jrpd4HNKWNoREkZnuW6rGkydAccOkd5aY5kNK
         ZSldLD0CANsIcedWM+FsDKLi1n8rcoWNuJnFyzrnEsKhc5Tn4UdDWAy33gxNxuunqnhV
         5H2xQ5pA+RJIrgZrqRTb3wsz8qCdUTSrKMks+43Tjv8AbQqOlUX+tpyGJ9gJBzLCIUgv
         BuUw==
X-Gm-Message-State: AGRZ1gI6n13fr+a+ImujXyCq9GMjQli+SIiWuXwILAz/YXqDeIxFYhjA
	GeqnKZvFsMb24IZCs3s8HwZPHw==
X-Google-Smtp-Source: AJdET5cW9RKtY8BLPxk+Ju7F6w9cWfTB9SsR/RvsWByGTZsILmz8zbMPhStb61dziW6mN9/tyDpmag==
X-Received: by 2002:a25:bf84:: with SMTP id l4-v6mr1679732ybk.100.1541654250222;
        Wed, 07 Nov 2018 21:17:30 -0800 (PST)
X-BeenThere: std-proposals@isocpp.org
Original-Received: by 2002:a81:51c3:: with SMTP id f186-v6ls599245ywb.1.gmail; Wed, 07
 Nov 2018 21:17:29 -0800 (PST)
X-Received: by 2002:a0d:eb4a:: with SMTP id u71-v6mr32617ywe.4.1541654248886;
        Wed, 07 Nov 2018 21:17:28 -0800 (PST)
In-Reply-To: <CA+EzHGdvL2k3CS+oeC7e8fmviEVj7PD2OLQiBEJLTf2QZMqUWA@mail.gmail.com>
X-Original-Sender: frankhb1989@gmail.com
Precedence: list
Mailing-list: list std-proposals@isocpp.org; contact std-proposals+owners@isocpp.org
List-ID: <std-proposals.isocpp.org>
X-Spam-Checked-In-Group: std-proposals@isocpp.org
X-Google-Group-Id: 399137483710
List-Post: <https://groups.google.com/a/isocpp.org/group/std-proposals/post>, <mailto:std-proposals@isocpp.org>
List-Help: <https://support.google.com/a/isocpp.org/bin/topic.py?topic=25838>, <mailto:std-proposals+help@isocpp.org>
List-Archive: <https://groups.google.com/a/isocpp.org/group/std-proposals/>
List-Subscribe: <https://groups.google.com/a/isocpp.org/group/std-proposals/subscribe>,
 <mailto:std-proposals+subscribe@isocpp.org>
List-Unsubscribe: <mailto:googlegroups-manage+399137483710+unsubscribe@googlegroups.com>,
 <https://groups.google.com/a/isocpp.org/group/std-proposals/subscribe>
Xref: news.gmane.org gmane.comp.lang.c++.isocpp.proposals:40916
Archived-At: <http://permalink.gmane.org/gmane.comp.lang.c++.isocpp.proposals/40916>

------=_Part_264_1437820450.1541654248247
Content-Type: multipart/alternative; 
	boundary="----=_Part_265_2069398245.1541654248247"

------=_Part_265_2069398245.1541654248247
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable



=E5=9C=A8 2018=E5=B9=B411=E6=9C=888=E6=97=A5=E6=98=9F=E6=9C=9F=E5=9B=9B UTC=
+8=E4=B8=8A=E5=8D=8810:56:55=EF=BC=8CVinnie Falco=E5=86=99=E9=81=93=EF=BC=
=9A
>
> On Wed, Nov 7, 2018 at 6:41 PM <mutant....@gmail.com <javascript:>>=20
> wrote:=20
> > Trying to remove infinite loops from c++ in order to be able to prove a=
=20
> program=20
> > can complete means these things can't be written in c++.=20
>
> This is a non-turing-complete language for which the halting problem=20
> is solvable:=20
>
> "Simplicity: A New Language for Blockchains"=20
> Simplicity is a typed, combinator-based, functional language without=20
> loops and recursion, designed to be used for crypto-currencies and=20
> blockchain applications.=20
> <https://blockstream.com/simplicity.pdf>=20
>
> Regards=20
>

This might be interesting (esp. the formal methods and the part of TCO to=
=20
me, compared to the disability of EVM), but does it target the domains=20
sufficiently close to C++ concerned here?

In fact, every language with proved strong normalization in rewriting=20
semantics is non-Turing-complete like this. And this is far from C++, even=
=20
far than well-reserarched STLC=20
<https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus>, which is=20
enough to show the property.

--=20
You received this message because you are subscribed to the Google Groups "=
ISO C++ Standard - Future Proposals" group.
To unsubscribe from this group and stop receiving emails from it, send an e=
mail to std-proposals+unsubscribe@isocpp.org.
To post to this group, send email to std-proposals@isocpp.org.
To view this discussion on the web visit https://groups.google.com/a/isocpp=
..org/d/msgid/std-proposals/987a5677-b6fd-46d0-8655-6e5c582a136a%40isocpp.or=
g.

------=_Part_265_2069398245.1541654248247
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr"><br><br>=E5=9C=A8 2018=E5=B9=B411=E6=9C=888=E6=97=A5=E6=98=
=9F=E6=9C=9F=E5=9B=9B UTC+8=E4=B8=8A=E5=8D=8810:56:55=EF=BC=8CVinnie Falco=
=E5=86=99=E9=81=93=EF=BC=9A<blockquote class=3D"gmail_quote" style=3D"margi=
n: 0;margin-left: 0.8ex;border-left: 1px #ccc solid;padding-left: 1ex;">On =
Wed, Nov 7, 2018 at 6:41 PM &lt;<a href=3D"javascript:" target=3D"_blank" g=
df-obfuscated-mailto=3D"4pNATMdWBAAJ" rel=3D"nofollow" onmousedown=3D"this.=
href=3D&#39;javascript:&#39;;return true;" onclick=3D"this.href=3D&#39;java=
script:&#39;;return true;">mutant....@gmail.com</a>&gt; wrote:
<br>&gt; Trying to remove infinite loops from c++ in order to be able to pr=
ove a program
<br>&gt; can complete means these things can&#39;t be written in c++.
<br>
<br>This is a non-turing-complete language for which the halting problem
<br>is solvable:
<br>
<br>&quot;Simplicity: A New Language for Blockchains&quot;
<br>Simplicity is a typed, combinator-based, functional language without
<br>loops and recursion, designed to be used for crypto-currencies and
<br>blockchain applications.
<br>&lt;<a href=3D"https://blockstream.com/simplicity.pdf" target=3D"_blank=
" rel=3D"nofollow" onmousedown=3D"this.href=3D&#39;https://www.google.com/u=
rl?q\x3dhttps%3A%2F%2Fblockstream.com%2Fsimplicity.pdf\x26sa\x3dD\x26sntz\x=
3d1\x26usg\x3dAFQjCNE-GXGMFlRXtBd3Sd-oz9q22SmSZg&#39;;return true;" onclick=
=3D"this.href=3D&#39;https://www.google.com/url?q\x3dhttps%3A%2F%2Fblockstr=
eam.com%2Fsimplicity.pdf\x26sa\x3dD\x26sntz\x3d1\x26usg\x3dAFQjCNE-GXGMFlRX=
tBd3Sd-oz9q22SmSZg&#39;;return true;">https://blockstream.com/<wbr>simplici=
ty.pdf</a>&gt;
<br>
<br>Regards
<br></blockquote><div><br>This might be interesting (esp. the formal method=
s and the part of TCO to me, compared to the disability of EVM), but does i=
t target the domains sufficiently close to C++ concerned here?<br><br>In fa=
ct, every language with proved strong normalization in rewriting semantics =
is non-Turing-complete like this. And this is far from C++, even far than w=
ell-reserarched <a href=3D"https://en.wikipedia.org/wiki/Simply_typed_lambd=
a_calculus">STLC</a>, which is enough to show the property.<br><br></div></=
div>

<p></p>

-- <br />
You received this message because you are subscribed to the Google Groups &=
quot;ISO C++ Standard - Future Proposals&quot; group.<br />
To unsubscribe from this group and stop receiving emails from it, send an e=
mail to <a href=3D"mailto:std-proposals+unsubscribe@isocpp.org">std-proposa=
ls+unsubscribe@isocpp.org</a>.<br />
To post to this group, send email to <a href=3D"mailto:std-proposals@isocpp=
..org">std-proposals@isocpp.org</a>.<br />
To view this discussion on the web visit <a href=3D"https://groups.google.c=
om/a/isocpp.org/d/msgid/std-proposals/987a5677-b6fd-46d0-8655-6e5c582a136a%=
40isocpp.org?utm_medium=3Demail&utm_source=3Dfooter">https://groups.google.=
com/a/isocpp.org/d/msgid/std-proposals/987a5677-b6fd-46d0-8655-6e5c582a136a=
%40isocpp.org</a>.<br />

------=_Part_265_2069398245.1541654248247--

------=_Part_264_1437820450.1541654248247--

.
