From mboxrd@z Thu Jan 1 00:00:00 1970 Path: news.gmane.io!.POSTED.blaine.gmane.org!not-for-mail From: Stephen Leake Newsgroups: gmane.emacs.devel Subject: Re: Ada (was Re: Tree Sitter) Date: Sun, 25 Jul 2021 22:05:34 -0700 Message-ID: <865ywx7jhd.fsf@stephe-leake.org> 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> Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable Injection-Info: ciao.gmane.io; posting-host="blaine.gmane.org:116.202.254.214"; logging-data="14198"; mail-complaints-to="usenet@ciao.gmane.io" User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/28.0.50 (windows-nt) Cc: Richard Stallman , emacs-devel@gnu.org To: "Perry E. Metzger" Original-X-From: emacs-devel-bounces+ged-emacs-devel=m.gmane-mx.org@gnu.org Mon Jul 26 07:06:26 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 1m7sor-0003XX-MV for ged-emacs-devel@m.gmane-mx.org; Mon, 26 Jul 2021 07:06:26 +0200 Original-Received: from localhost ([::1]:40760 helo=lists1p.gnu.org) by lists.gnu.org with esmtp (Exim 4.90_1) (envelope-from ) id 1m7soq-0007ZO-Le for ged-emacs-devel@m.gmane-mx.org; Mon, 26 Jul 2021 01:06:24 -0400 Original-Received: from eggs.gnu.org ([2001:470:142:3::10]:42424) by lists.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1m7soB-0006oS-6J for emacs-devel@gnu.org; Mon, 26 Jul 2021 01:05:43 -0400 Original-Received: from gateway22.websitewelcome.com ([192.185.46.152]:46201) by eggs.gnu.org with esmtps (TLS1.2:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.90_1) (envelope-from ) id 1m7so7-0000gY-6Q for emacs-devel@gnu.org; Mon, 26 Jul 2021 01:05:42 -0400 Original-Received: from cm13.websitewelcome.com (cm13.websitewelcome.com [100.42.49.6]) by gateway22.websitewelcome.com (Postfix) with ESMTP id 9974A934E for ; Mon, 26 Jul 2021 00:05:37 -0500 (CDT) Original-Received: from host2007.hostmonster.com ([67.20.76.71]) by cmsmtp with SMTP id 7so5m4JbfrJtZ7so5mqAvx; Mon, 26 Jul 2021 00:05:37 -0500 X-Authority-Reason: nr=8 DKIM-Signature: v=1; a=rsa-sha256; q=dns/txt; c=relaxed/relaxed; d=stephe-leake.org; s=default; h=Content-Transfer-Encoding:Content-Type: MIME-Version:Message-ID:In-Reply-To:Date:References:Subject:Cc:To:From:Sender :Reply-To:Content-ID:Content-Description:Resent-Date:Resent-From: Resent-Sender:Resent-To:Resent-Cc:Resent-Message-ID:List-Id:List-Help: List-Unsubscribe:List-Subscribe:List-Post:List-Owner:List-Archive; bh=8JLDV/Ahiywh2lms4i+xfcKpdJsEkxlMtEaOADbCmXE=; b=gDDiXOetClrhFSNiOov4Xpja6i N6/mtSKUXG1n1cnIyS4QoWmduCO2+/zjkI38aBulaZnNiRb8Dj9kzSSQeka14i1cXIbzHcXumDfaX 4XG+WVvzCjR6p+yFFwk8x5kCjrb7UbiQq8mLr+c8GaakAblFHwtkIIjxdmvnAcckblMPmCiOQWBTn otY6lDG8GNzYOR3J4MkuJpig7J/y/HpJLGfh6860jf6FlNQ1hL77CxTYR3EzhGhTYx2KGwW6ivnJw cBKE1q8NR+TNRG9hDtfVoyAl0n1fDyfk2RY31Ey2La/HtYrrbgXArwG2S8nHOWni15Mf6VRckIeLA c/sPIpJg==; Original-Received: from [76.77.182.20] (port=58953 helo=Takver4) by host2007.hostmonster.com with esmtpsa (TLS1.2) tls TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384 (Exim 4.94.2) (envelope-from ) id 1m7so4-003nyq-Rw; Sun, 25 Jul 2021 23:05:36 -0600 In-Reply-To: (Perry E. Metzger's message of "Sun, 25 Jul 2021 15:52:51 -0400") X-AntiAbuse: This header was added to track abuse, please include it with any abuse report X-AntiAbuse: Primary Hostname - host2007.hostmonster.com X-AntiAbuse: Original Domain - gnu.org X-AntiAbuse: Originator/Caller UID/GID - [47 12] / [47 12] X-AntiAbuse: Sender Address Domain - stephe-leake.org X-BWhitelist: no X-Source-IP: 76.77.182.20 X-Source-L: No X-Exim-ID: 1m7so4-003nyq-Rw X-Source-Sender: (Takver4) [76.77.182.20]:58953 X-Source-Auth: stephen_leake@stephe-leake.org X-Email-Count: 3 X-Source-Cap: c3RlcGhlbGU7c3RlcGhlbGU7aG9zdDIwMDcuaG9zdG1vbnN0ZXIuY29t X-Local-Domain: yes Received-SPF: permerror client-ip=192.185.46.152; envelope-from=stephen_leake@stephe-leake.org; helo=gateway22.websitewelcome.com X-Spam_score_int: -8 X-Spam_score: -0.9 X-Spam_bar: / X-Spam_report: (-0.9 / 5.0 requ) BAYES_00=-1.9, DKIM_INVALID=0.1, DKIM_SIGNED=0.1, RCVD_IN_DNSWL_NONE=-0.0001, RCVD_IN_MSPIKE_H2=-0.001, SPF_HELO_PASS=-0.001, SPF_NEUTRAL=0.779 autolearn=no 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:271630 Archived-At: "Perry E. Metzger" writes: > 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. > 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=C2=A0 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. > 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 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. In my defense, I started wisi when Ada was still very current, before Rust was 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 :). > 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. ok. >>> 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. Ok; that says nothing about whether it is better than wisi. I propose a metric in my draft paper on wisitoken error correction [1]; length of 'diff' output on the corrected token list. (WisiToken is the name of the parser generator/runtime used by the Gnu ELPA wisi package). By that metric, on the set of files I used, wisitoken error correction is better. I made wisitoken error correction that robust in order to meet the demands of indenting in the face of syntax errors. I've read the papers provided as references for tree-sitter error correction; it is not as powerful as wisi. For example, it does not consider inserting tokens to fix the error, which is essential when parsing a half-typed statement. > 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. Ok, I missed that (I'd much rather read a document than watch a video). I found https://codeberg.org/FelipeLema/tree-sitter-indent.el; I'll have to play with it. >> 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. 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 -- -- Stephe [1] https://stephe-leake.org/ada/error_correction_algorithm.pdf