From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.io!.POSTED.blaine.gmane.org!not-for-mail From: "Perry E. Metzger" Newsgroups: gmane.emacs.devel Subject: Re: Ada (was Re: Tree Sitter) Date: Mon, 26 Jul 2021 10:01:53 -0400 Message-ID: <5766153d-8229-f803-5409-4a396c43a108@piermont.com> References: <62e438b5-d27f-1d3c-69c6-11fe29a76d74@dancol.org> <83fsxsdxhu.fsf@gnu.org> <179f22a44d8.2816.cc5b3318d7e9908e2c46732289705cb0@dancol.org> <179f38c0370.2816.cc5b3318d7e9908e2c46732289705cb0@dancol.org> <236e62c2-be9b-b26d-8cd0-4b5a1a86e19a@dancol.org> <86mtqsoh3f.fsf@stephe-leake.org> <286d815e-d1a1-07ca-6696-a7f51923ab4e@piermont.com> <86wnpl6f0y.fsf@stephe-leake.org> <865yx45y7g.fsf@stephe-leake.org> <146b72ac-0446-93ba-f85c-b8987e96f0d0@piermont.com> <86eebm8j7d.fsf@stephe-leake.org> <865ywx7jhd.fsf@stephe-leake.org> <86tukh5s2w.fsf@stephe-leake.org> Mime-Version: 1.0 Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 8bit Injection-Info: ciao.gmane.io; posting-host="blaine.gmane.org:116.202.254.214"; logging-data="24481"; mail-complaints-to="usenet@ciao.gmane.io" User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.15; rv:91.0) Gecko/20100101 Thunderbird/91.0 Cc: emacs-devel@gnu.org To: Stephen Leake Original-X-From: emacs-devel-bounces+ged-emacs-devel=m.gmane-mx.org@gnu.org Mon Jul 26 16:03:06 2021 Return-path: Envelope-to: ged-emacs-devel@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 1m81CD-000687-MY for ged-emacs-devel@m.gmane-mx.org; Mon, 26 Jul 2021 16:03:05 +0200 Original-Received: from localhost ([::1]:57552 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1m81CC-0002EO-LO for ged-emacs-devel@m.gmane-mx.org; Mon, 26 Jul 2021 10:03:04 -0400 Original-Received: from eggs.gnu.org ([2001:470:142:3::10]:37560) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1m81B7-00008a-7v for emacs-devel@gnu.org; Mon, 26 Jul 2021 10:01:57 -0400 Original-Received: from hacklheber.piermont.com ([166.84.7.14]:38482) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1m81B5-0001WH-AY for emacs-devel@gnu.org; Mon, 26 Jul 2021 10:01:56 -0400 Original-Received: from snark.cb.piermont.com (localhost [127.0.0.1]) by hacklheber.piermont.com (Postfix) with UTF8SMTP id E0C6567; Mon, 26 Jul 2021 10:01:53 -0400 (EDT) Original-Received: from [10.160.2.107] (jabberwock.cb.piermont.com [10.160.2.107]) by snark.cb.piermont.com (Postfix) with UTF8SMTP id ACAD52DE2C4; Mon, 26 Jul 2021 10:01:53 -0400 (EDT) Content-Language: en-US In-Reply-To: <86tukh5s2w.fsf@stephe-leake.org> Received-SPF: pass client-ip=166.84.7.14; envelope-from=perry@piermont.com; helo=hacklheber.piermont.com X-Spam_score_int: -22 X-Spam_score: -2.3 X-Spam_bar: -- X-Spam_report: (-2.3 / 5.0 requ) BAYES_00=-1.9, NICE_REPLY_A=-0.438, SPF_HELO_NONE=0.001, SPF_PASS=-0.001 autolearn=ham autolearn_force=no X-Spam_action: no action X-BeenThere: emacs-devel@gnu.org X-Mailman-Version: 2.1.23 Precedence: list List-Id: "Emacs development discussions." List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: emacs-devel-bounces+ged-emacs-devel=m.gmane-mx.org@gnu.org Original-Sender: "Emacs-devel" Xref: news.gmane.io gmane.emacs.devel:271649 Archived-At: On 7/26/21 05:42, Stephen Leake wrote: > Stephen Leake writes: > >>> There are far more modern systems programming languages out there >>> (like Rust) that statically guarantee far more, including that use >>> after free is impossible, that  threads cannot have data races, that >>> null pointers cannot exist. This should not be surprising, as type >>> theory (and programming language theory in general) has advanced >>> dramatically in the last 40 years. >> Ada has kept up with some of that; the next ISO version is due in >> 2022. > The current Ada/SPARK allows enforcing the ownership model for pointers. > Ada 2022 has structures supporting parallelizing loops and blocks. > A separation logic like SPARK is necessarily going to have tools to track pointers. That's rather different from the general language itself being able to do that. Vectorizing loops is cool but not in the same class as what Rust makes possible. But I really think we should drop this, it's not Emacs related any more. Perry