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 09:45:40 -0400 Message-ID: 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> 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="24919"; 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 15:47:00 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 1m80we-0006G6-5b for ged-emacs-devel@m.gmane-mx.org; Mon, 26 Jul 2021 15:47:00 +0200 Original-Received: from localhost ([::1]:43118 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1m80wd-00008M-7N for ged-emacs-devel@m.gmane-mx.org; Mon, 26 Jul 2021 09:46:59 -0400 Original-Received: from eggs.gnu.org ([2001:470:142:3::10]:33312) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1m80vQ-0007MF-64 for emacs-devel@gnu.org; Mon, 26 Jul 2021 09:45:44 -0400 Original-Received: from hacklheber.piermont.com ([166.84.7.14]:38410) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1m80vO-0006oN-9x for emacs-devel@gnu.org; Mon, 26 Jul 2021 09:45:43 -0400 Original-Received: from snark.cb.piermont.com (localhost [127.0.0.1]) by hacklheber.piermont.com (Postfix) with UTF8SMTP id 1AAFE67; Mon, 26 Jul 2021 09:45:41 -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 D91AD2DE2C4; Mon, 26 Jul 2021 09:45:40 -0400 (EDT) Content-Language: en-US In-Reply-To: <865ywx7jhd.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:271648 Archived-At: On 7/26/21 01:05, Stephen Leake wrote: > "Perry E. Metzger" 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. I'm sure that improvements are being worked on, but the state of the art in language design really has moved on. No version of Ada has affine types, and no version of Ada _could_ get affine types without breaking the entire existing codebase. It's not easy to retrofit it to the language without completely altering the language. If you start working in a language with linear or affine types you will immediately see why. I agree that strongly typed languages with detection of array bounds violations and other undefined behavior are superior. Your own experience is evidence for that. You got lots of years of good work done in Ada that would not have been as easy in languages like C or C++. I agree those languages are full of traps for the unwary. I do not think, however, that Ada is the best choice for any new project being undertaken today. As I said, the state of the art has advanced dramatically in 40 years. > >> Rust in particular is an excellent language, and in addition to >> superior safety, has far better ergonomics. > I have heard good things about Rust, and some of the tree-sitter > infrastructure is written in Rust. I guess it's time to take my own > advice and learn a new language. > > Rewritting wisi in Rust would be an interesting challenge. Although I'm > not clear that would make it more acceptable to the Emacs project. I think you should try it anyway. At very worst, you will learn a great deal. You might also produce a library of interest to other people, and I think having more tools of this sort in the world is better. That said, I think for good or ill, the current iteration of Emacs works best with code written in C. That might eventually change, of course. Even the Linux kernel is now getting support for code written in Rust. Perhaps eventually, with the arrival of better and better versions of the Rust GCC front end and other tools, it will make sense for Emacs to have a mixed implementation. I don't think that time has arrived yet. (BTW, note that Tree Sitter is not written in Rust, though it does have a Rust API available.) >>> In addition, SPARK (https://www.adacore.com/sparkpro) is a formal proof >>> system designed for Ada, giving you even more power to build programs >>> that are correct. >> Yes, and for C I can use VST from Princeton for the same purpose (VST >> being a Coq-based separation logic based on CompCert), there are >> several other formal semantics for C that can be used for the same >> purpose (including other Coq based CompCert derived semantics as well >> as the K based semantics done by Chucky Ellison), and the Rustbelt >> project (not yet quite as production ready) provides a Coq semantics >> for Rust with which can be used for the same purpose. > So Ada/SPARK is better than Rust/Rustbelt here :). For now, but if I had to write a small high assurance real time kernel at the moment, I'd probably write it in a little language embedded in straight Coq with extraction to something with an efficient compiler (like Rust) even if the extraction wasn't verified. > >> Tree sitter can handle arbitrary LR and GLR grammars. > The Ada grammar is GLR; that's why wisi can handle it. I reported > tree-sitter not being able to handle Ada here: > https://github.com/tree-sitter/tree-sitter/issues/693 Thank you for reporting that. Perry