From: Stephen Leake <stephen_leake@stephe-leake.org>
To: "Perry E. Metzger" <perry@piermont.com>
Cc: Richard Stallman <rms@gnu.org>, emacs-devel@gnu.org
Subject: Re: Ada (was Re: Tree Sitter)
Date: Sun, 25 Jul 2021 22:05:34 -0700 [thread overview]
Message-ID: <865ywx7jhd.fsf@stephe-leake.org> (raw)
In-Reply-To: <e066afbb-0932-b4c6-f3d2-836d3c4c3661@piermont.com> (Perry E. Metzger's message of "Sun, 25 Jul 2021 15:52:51 -0400")
"Perry E. Metzger" <perry@piermont.com> 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 <rms@gnu.org> 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.
<snip>
> 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.
> 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
next prev parent reply other threads:[~2021-07-26 5:05 UTC|newest]
Thread overview: 274+ messages / expand[flat|nested] mbox.gz Atom feed top
2021-06-04 3:16 cc-mode fontification feels random Daniel Colascione
2021-06-04 6:10 ` Eli Zaretskii
2021-06-04 7:10 ` Theodor Thornhill
2021-06-04 10:08 ` João Távora
2021-06-04 10:39 ` Eli Zaretskii
2021-06-04 10:59 ` Philipp
2021-06-04 11:05 ` João Távora
2021-06-04 11:22 ` Eli Zaretskii
2021-06-04 12:44 ` Dmitry Gutov
2021-06-04 13:46 ` João Távora
2021-06-04 14:11 ` Eli Zaretskii
2021-06-04 11:18 ` Eli Zaretskii
2021-06-04 16:43 ` Jim Porter
[not found] ` <83k0n9l9pv.fsf@gnu.org>
2021-06-04 19:41 ` Jim Porter
2021-06-04 19:53 ` Eli Zaretskii
2021-06-04 20:05 ` Jim Porter
2021-06-04 20:11 ` Joost Kremers
2021-06-05 6:51 ` Eli Zaretskii
2021-06-05 10:14 ` Joost Kremers
2021-06-05 11:31 ` Eli Zaretskii
2021-06-05 12:12 ` Joost Kremers
2021-06-05 13:23 ` Stefan Monnier
2021-06-05 17:08 ` Óscar Fuentes
2021-06-05 17:31 ` Stefan Monnier
2021-06-05 17:32 ` Eli Zaretskii
2021-06-05 18:46 ` João Távora
2021-06-05 6:41 ` Eli Zaretskii
2021-06-05 9:32 ` João Távora
2021-06-05 9:59 ` Ergus
2021-06-05 11:29 ` Eli Zaretskii
2021-06-05 11:55 ` Daniel Colascione
2021-06-05 12:27 ` Eli Zaretskii
2021-06-05 17:59 ` Jim Porter
2021-06-05 18:56 ` Daniel Martín
2021-06-05 12:43 ` Ergus
2021-06-05 13:59 ` Remote GUI Emacs really works (was: cc-mode fontification feels random) Óscar Fuentes
2021-06-05 11:25 ` cc-mode fontification feels random Eli Zaretskii
2021-06-05 9:46 ` Ergus
2021-06-05 11:27 ` Eli Zaretskii
2021-06-04 20:14 ` Yuri Khan
2021-06-04 10:25 ` Eli Zaretskii
2021-06-04 10:05 ` Daniel Colascione
2021-06-04 10:22 ` Eli Zaretskii
2021-06-04 10:34 ` João Távora
2021-06-04 10:43 ` Eli Zaretskii
2021-06-04 18:25 ` Stefan Monnier
2021-06-04 18:36 ` Daniel Colascione
2021-06-04 19:11 ` Eli Zaretskii
2021-06-04 19:16 ` Daniel Colascione
2021-06-04 19:26 ` Eli Zaretskii
2021-06-04 19:33 ` Daniel Colascione
2021-06-04 19:51 ` Eli Zaretskii
2021-06-05 0:29 ` Stefan Monnier
2021-06-05 6:32 ` Eli Zaretskii
2021-06-04 19:07 ` Eli Zaretskii
2021-06-04 19:26 ` Daniel Colascione
2021-06-04 19:32 ` Eli Zaretskii
2021-06-04 10:41 ` Eli Zaretskii
2021-06-04 10:42 ` Ergus
2021-06-04 15:54 ` Alan Mackenzie
2021-06-04 18:30 ` Daniel Colascione
2021-06-06 11:37 ` Alan Mackenzie
2021-06-06 11:57 ` Eli Zaretskii
2021-06-06 12:27 ` Alan Mackenzie
2021-06-06 12:44 ` Eli Zaretskii
2021-06-06 14:19 ` Alan Mackenzie
2021-06-06 17:06 ` Eli Zaretskii
2021-06-06 17:44 ` Stefan Monnier
2021-06-06 18:00 ` Eli Zaretskii
2021-06-06 18:18 ` Stefan Monnier
2021-06-06 18:33 ` Daniel Colascione
2021-06-06 20:24 ` Stefan Monnier
2021-06-06 20:27 ` Daniel Colascione
2021-06-06 20:38 ` Stefan Monnier
2021-06-06 19:03 ` Eli Zaretskii
2021-06-06 20:28 ` Stefan Monnier
2021-06-07 7:35 ` martin rudalics
2021-06-07 13:20 ` Stefan Monnier
2021-06-07 13:37 ` Eli Zaretskii
2021-06-08 0:06 ` Daniel Colascione
2021-06-08 15:16 ` Stefan Monnier
2021-06-07 15:58 ` martin rudalics
2021-06-08 4:01 ` Richard Stallman
2021-06-08 15:29 ` Stefan Monnier
2021-06-08 15:52 ` Eli Zaretskii
2021-06-08 16:36 ` Stefan Monnier
2021-06-08 18:11 ` Daniel Colascione
2021-06-08 18:25 ` Eli Zaretskii
2021-06-08 18:28 ` Daniel Colascione
2021-06-08 18:54 ` Eli Zaretskii
2021-06-09 18:22 ` Alan Mackenzie
2021-06-09 18:36 ` Eli Zaretskii
2021-06-09 18:51 ` Daniel Colascione
2021-06-09 19:04 ` Eli Zaretskii
2021-06-09 20:07 ` chad
2021-06-10 6:43 ` Eli Zaretskii
2021-06-09 20:17 ` Dmitry Gutov
2021-06-09 21:03 ` Alan Mackenzie
2021-06-10 2:21 ` Daniel Colascione
2021-06-10 6:55 ` Eli Zaretskii
2021-06-10 6:58 ` Daniel Colascione
2021-06-10 7:19 ` Eli Zaretskii
2021-06-10 6:39 ` Eli Zaretskii
2021-06-10 16:46 ` Alan Mackenzie
2021-06-10 17:01 ` Eli Zaretskii
2021-06-10 17:07 ` Daniel Colascione
2021-06-10 17:22 ` Eli Zaretskii
2021-06-10 17:33 ` Daniel Colascione
2021-06-10 17:39 ` Eli Zaretskii
2021-06-10 17:40 ` Óscar Fuentes
2021-06-10 17:44 ` Eli Zaretskii
2021-06-11 16:11 ` Alan Mackenzie
2021-06-11 17:53 ` Eli Zaretskii
2021-06-11 18:02 ` Daniel Colascione
2021-06-11 18:22 ` Eli Zaretskii
2021-06-11 18:28 ` Daniel Colascione
2021-06-11 19:12 ` Alan Mackenzie
2021-06-11 19:23 ` Eli Zaretskii
2021-06-11 18:47 ` Alan Mackenzie
2021-06-11 19:32 ` Eli Zaretskii
2021-06-11 19:46 ` Alan Mackenzie
2021-06-11 19:50 ` Eli Zaretskii
2021-06-11 18:42 ` Stefan Monnier
2021-06-11 19:31 ` Eli Zaretskii
2021-06-11 19:57 ` Stefan Monnier
2021-06-11 23:25 ` Ergus
2021-06-11 23:52 ` Óscar Fuentes
2021-06-12 1:08 ` Ergus
2021-06-12 3:20 ` Stefan Monnier
2021-06-12 11:07 ` Ergus
2021-06-12 6:58 ` Eli Zaretskii
2021-06-12 11:01 ` Ergus
2021-06-12 11:25 ` Eli Zaretskii
2021-06-12 15:04 ` Ergus
2021-06-12 15:16 ` Eli Zaretskii
2021-06-12 15:23 ` Ergus
2021-06-12 15:35 ` Eli Zaretskii
2021-06-12 14:00 ` Stefan Monnier
2021-06-12 14:20 ` Eli Zaretskii
2021-06-12 14:33 ` Stefan Monnier
2021-06-12 15:06 ` Eli Zaretskii
2021-06-12 15:46 ` Stefan Monnier
2021-06-12 6:50 ` Eli Zaretskii
2021-06-12 5:20 ` Theodor Thornhill
2021-06-12 13:40 ` Stefan Monnier
2021-06-12 15:56 ` Theodor Thornhill
2021-06-12 16:59 ` Ergus
2021-06-12 17:51 ` Theodor Thornhill
2021-06-12 17:25 ` Stefan Monnier
2021-06-12 17:53 ` Theodor Thornhill
2021-06-12 17:54 ` Ergus
2021-06-12 18:02 ` Daniel Colascione
2021-06-12 18:39 ` Ergus
2021-06-12 6:38 ` Eli Zaretskii
2021-06-12 13:44 ` Stefan Monnier
2021-06-12 14:14 ` Eli Zaretskii
2021-06-11 20:06 ` Alan Mackenzie
2021-06-12 6:44 ` Eli Zaretskii
2021-06-12 8:00 ` Daniel Colascione
2021-06-12 8:08 ` Eli Zaretskii
2021-06-12 9:31 ` Alan Mackenzie
2021-06-11 19:48 ` Eli Zaretskii
2021-06-11 18:34 ` Alan Mackenzie
2021-06-10 17:26 ` Óscar Fuentes
2021-06-10 17:39 ` andrés ramírez
2021-06-10 21:06 ` Stefan Monnier
2021-06-11 6:14 ` Eli Zaretskii
2021-06-10 15:16 ` Ergus
2021-06-10 15:34 ` Óscar Fuentes
2021-06-10 19:06 ` Ergus
2021-06-10 19:28 ` Eli Zaretskii
2021-06-10 21:56 ` Ergus
2021-06-10 15:59 ` Jim Porter
2021-06-10 21:02 ` Stefan Monnier
2021-06-11 20:21 ` Ergus
2021-06-11 20:27 ` Stefan Monnier
2021-06-11 20:37 ` Daniel Colascione
2021-06-11 20:52 ` Stefan Monnier
2021-06-12 6:46 ` Eli Zaretskii
2021-06-12 8:03 ` Daniel Colascione
2021-06-12 8:13 ` Eli Zaretskii
2021-06-12 13:51 ` Stefan Monnier
2021-06-12 8:47 ` Daniele Nicolodi
2021-06-12 8:57 ` tomas
2021-06-12 14:04 ` Stefan Monnier
2021-06-09 19:05 ` Daniel Colascione
2021-06-09 19:11 ` Eli Zaretskii
2021-06-09 20:20 ` Alan Mackenzie
2021-06-09 20:36 ` Stefan Monnier
2021-06-10 7:01 ` Daniel Colascione
2021-06-10 7:21 ` Eli Zaretskii
2021-06-10 2:21 ` Daniel Colascione
2021-06-19 9:25 ` Alan Mackenzie
2021-06-19 15:24 ` Alan Mackenzie
2021-07-09 14:06 ` Daniel Colascione
2021-07-11 18:12 ` Stephen Leake
2021-07-15 18:13 ` Perry E. Metzger
2021-07-15 22:43 ` Tree Sitter (was Re: cc-mode fontification feels random) Perry E. Metzger
2021-07-19 23:49 ` Stephen Leake
2021-07-20 14:53 ` Perry E. Metzger
2021-07-21 0:04 ` Stephen Leake
2021-07-21 1:28 ` Stefan Monnier
2021-07-21 14:43 ` Perry E. Metzger
2021-07-21 16:21 ` Daniel Colascione
2021-07-21 19:15 ` Perry E. Metzger
2021-07-22 1:16 ` Daniel Colascione
2021-07-22 13:18 ` Perry E. Metzger
2021-07-22 13:49 ` Yuan Fu
2021-07-24 20:05 ` [SPAM UNSURE] " Stephen Leake
2021-07-25 0:41 ` Daniel Colascione
2021-07-26 4:24 ` [SPAM UNSURE] " Stephen Leake
2021-07-25 18:01 ` Perry E. Metzger
2021-07-22 14:00 ` Perry E. Metzger
2021-07-24 1:17 ` Richard Stallman
2021-07-25 16:13 ` Stephen Leake
2021-07-25 19:52 ` Ada (was Re: Tree Sitter) Perry E. Metzger
2021-07-26 5:05 ` Stephen Leake [this message]
2021-07-26 9:42 ` Stephen Leake
2021-07-26 14:01 ` Perry E. Metzger
2021-07-26 13:45 ` Perry E. Metzger
2021-07-27 0:26 ` Richard Stallman
2021-07-27 12:38 ` Perry E. Metzger
2021-07-26 2:23 ` Tree Sitter (was Re: cc-mode fontification feels random) John Yates
2021-07-24 19:59 ` Stephen Leake
2021-07-24 21:21 ` OFF-TOPIC: Ada availability (was: Tree Sitter) Óscar Fuentes
2021-07-25 7:31 ` tomas
2021-06-08 18:11 ` cc-mode fontification feels random Eli Zaretskii
2021-06-08 21:25 ` Stefan Monnier
2021-06-09 3:39 ` Richard Stallman
2021-06-09 8:34 ` martin rudalics
2021-06-09 13:14 ` `open-paren-in-column-0-is-defun-start` (was: cc-mode fontification feels random) Stefan Monnier
2021-06-09 15:15 ` Yuri Khan
2021-06-09 15:16 ` Yuri Khan
2021-06-12 17:29 ` cc-mode fontification feels random João Távora
2021-06-13 8:50 ` martin rudalics
2021-06-13 9:05 ` João Távora
2021-06-13 9:39 ` martin rudalics
2021-06-13 10:06 ` João Távora
2021-06-13 14:52 ` martin rudalics
2021-06-13 15:25 ` João Távora
2021-06-14 8:29 ` martin rudalics
2021-06-14 8:40 ` João Távora
2021-06-14 9:00 ` martin rudalics
2021-06-14 9:14 ` João Távora
2021-06-14 11:28 ` Eli Zaretskii
2021-06-14 14:39 ` Stefan Monnier
2021-06-15 22:38 ` Ergus
2021-06-07 12:08 ` Eli Zaretskii
2021-06-08 15:22 ` Stefan Monnier
2021-06-08 15:46 ` Eli Zaretskii
2021-06-05 20:25 ` Dmitry Gutov
2021-06-06 11:53 ` Alan Mackenzie
2021-06-06 17:08 ` Dmitry Gutov
2021-08-30 18:50 ` [PATCH] " Alan Mackenzie
2021-08-30 19:03 ` Perry E. Metzger
2021-08-30 19:18 ` Alan Mackenzie
2021-08-30 19:25 ` Eli Zaretskii
2021-08-30 19:28 ` Daniel Colascione
2021-08-30 19:37 ` Eli Zaretskii
2021-08-30 20:11 ` Stefan Monnier
2021-08-31 10:54 ` Alan Mackenzie
2021-08-31 13:23 ` Eli Zaretskii
2021-08-31 16:02 ` Alan Mackenzie
2021-08-31 16:21 ` Eli Zaretskii
2021-08-31 16:46 ` Alan Mackenzie
2021-08-31 17:02 ` Eli Zaretskii
2021-08-31 18:56 ` Stefan Monnier
2021-08-31 21:17 ` Alan Mackenzie
2021-08-31 21:47 ` Stefan Monnier
2021-10-22 20:13 ` [Committed PATCH] " Alan Mackenzie
2021-10-24 20:18 ` Alan Mackenzie
2021-08-31 13:18 ` [PATCH] " Eli Zaretskii
2021-08-30 20:03 ` Alan Mackenzie
2021-08-31 11:53 ` Eli Zaretskii
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
List information: https://www.gnu.org/software/emacs/
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=865ywx7jhd.fsf@stephe-leake.org \
--to=stephen_leake@stephe-leake.org \
--cc=emacs-devel@gnu.org \
--cc=perry@piermont.com \
--cc=rms@gnu.org \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
Code repositories for project(s) associated with this public inbox
https://git.savannah.gnu.org/cgit/emacs.git
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).