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: Ada (was Re: Tree Sitter) Date: Sun, 25 Jul 2021 15:52:51 -0400 Message-ID: References: <83o8cge4lg.fsf@gnu.org> <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> Mime-Version: 1.0 Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 7bit Injection-Info: ciao.gmane.io; posting-host="blaine.gmane.org:116.202.254.214"; logging-data="27684"; 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 , Richard Stallman Original-X-From: emacs-devel-bounces+ged-emacs-devel=m.gmane-mx.org@gnu.org Sun Jul 25 21:53:34 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 1m7kBp-00070R-Km for ged-emacs-devel@m.gmane-mx.org; Sun, 25 Jul 2021 21:53:33 +0200 Original-Received: from localhost ([::1]:33498 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1m7kBo-0005Xj-MU for ged-emacs-devel@m.gmane-mx.org; Sun, 25 Jul 2021 15:53:32 -0400 Original-Received: from eggs.gnu.org ([2001:470:142:3::10]:47954) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1m7kBD-0004TQ-Oq for emacs-devel@gnu.org; Sun, 25 Jul 2021 15:52:55 -0400 Original-Received: from hacklheber.piermont.com ([166.84.7.14]:36350) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1m7kBB-0008Ge-Dj; Sun, 25 Jul 2021 15:52:55 -0400 Original-Received: from snark.cb.piermont.com (localhost [127.0.0.1]) by hacklheber.piermont.com (Postfix) with UTF8SMTP id C94D32AC; Sun, 25 Jul 2021 15:52:51 -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 5E5182DE862; Sun, 25 Jul 2021 15:52:51 -0400 (EDT) Content-Language: en-US In-Reply-To: <86eebm8j7d.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: -18 X-Spam_score: -1.9 X-Spam_bar: - X-Spam_report: (-1.9 / 5.0 requ) BAYES_00=-1.9, CTE_8BIT_MISMATCH=0.001, 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:271624 Archived-At: This is getting off topic, so I've changed the Subject: line. It probably shouldn't continue to be pursued here, this entire response may be seriously past what should be on the -devel list and I don't blame people for tuning out. On 7/25/21 12:13, Stephen Leake wrote: > Richard Stallman writes: > >> >> The features that the DoD liked so much about Ada, to me make it feel >> very clunky. You have to declare so much! > Yes, and then the compiler checks everything for you, so the code is > much more likely to be correct before you start testing. > > It also helps when modifying/extending code; if it doesn't compile, > you've done something wrong, and the error messages point to what to > fix. The Ada compiler doesn't actually statically guarantee all safety. In particular, issues like concurrency safety violations, use after free, null pointer dereference, etc. are all possible in Ada. It's better than C certainly, as it provides for things like array bounds checking and has a strong static type system, but Ada is very much an early 1980s language and it shows. 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. Rust in particular is an excellent language, and in addition to superior safety, has far better ergonomics. I honestly cannot see why anyone would write a program now in Ada rather than in Rust if their interest was high assurance combined with high programmer productivity. There is no axis on which Ada is superior, and many on which it is far worse. All that said, I _can_ think of good reasons to work in C when dealing with GNU Emacs, most specifically, that Emacs is (at least currently) written in C. Use of a language like Ada makes the tooling situation for a potential user much less pleasant. > 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. There are two formally verified operating system kernels in existence, SEL4 and CertiKOS. Both are written in C. I don't think working in C is an optimal path to creating such systems, it's a dangerous language, but I do want to point out that SPARK is nothing special at this point. > A long time ago, I was working on a system that was programmed in C++. I > re-implemented it in Ada; it was pretty clear that I could write correct > code at least 4 times faster in Ada than in C++. Now I only write code > in something other than Ada if there is no way to use Ada (for example, > my music app on Android is in Java; it's nominally possible to write Ada > code for Android, but it takes a _lot_ of work, and would break with > every new release of Android). > I recommend you try out Rust. That said, it, too, is not the right path for writing Android apps. >> What advantages does wisi.el's Ada module have over Tree Sitter? > That's not entirely clear yet. I believe the error recovery in wisi is > more powerful than tree-sitter's, but I'm probably biased, and it's > hard to come up with a good objective metric until we get both fully > integrated into Emacs. It is clear that good error recovery is essential > to implementing indentation using a parser; tree-sitter is not > advertised as supporting indentation, while indentation is a primary > purpose of wisi. Error recovery in Tree Sitter is excellent. Tree sitter has also been used for indentation. The videos presenting Tree Sitter make it clear that font highlighting, code folding, indentation and many other purposes are all envisioned for the library. > > The parser generator in wisi is more powerful in some ways; it can > handle LR1 table generation for Ada, using a grammar that closely > follows the grammar in the Ada Language Reference Manual; tree-sitter > can't handle that. tree-sitter could probably handle it if someone > spends time simplifying/optimizing the grammar. Tree sitter can handle arbitrary LR and GLR grammars. Almost any other grammar for a real programming language (say an LL1 grammar) can be mechanically transformed into one of those. > The tree-sitter parser generator allows specifying token precedence to > resolve grammar conflicts; wisi has no support for that (it could be > added). > > tree-sitter has been around for a while, and there are many people and > editors using it and working on it. wisi is just me working on it, and > Emacs using it for ada-mode. > > tree-sitter also provides bindings to the parser for other languages. > That is possible with wisi, but I don't have the bandwidth for it. > Generally, I'm in favor of people trying experiments. People should spend their time however they like, and should follow wherever their muse takes them. This is how we learn. I encourage you to keep working on your project. However, in the current circumstance, I suspect that the wisi effort is less likely to produce a robust result that Emacs can rely on. It is written in a language not generally used for Emacs code. It is being worked on by single individual instead of a large community. It does not currently have obvious advantages in terms of features. Perry