[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Ada (was Re: Tree Sitter)
From: |
Stephen Leake |
Subject: |
Re: Ada (was Re: Tree Sitter) |
Date: |
Sun, 25 Jul 2021 22:05:34 -0700 |
User-agent: |
Gnus/5.13 (Gnus v5.13) Emacs/28.0.50 (windows-nt) |
"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
- Re: Tree Sitter (was Re: cc-mode fontification feels random), (continued)
- Re: Tree Sitter (was Re: cc-mode fontification feels random), Perry E. Metzger, 2021/07/22
- Re: Tree Sitter (was Re: cc-mode fontification feels random), Yuan Fu, 2021/07/22
- Re: [SPAM UNSURE] Re: Tree Sitter (was Re: cc-mode fontification feels random), Stephen Leake, 2021/07/24
- Re: [SPAM UNSURE] Re: Tree Sitter (was Re: cc-mode fontification feels random), Daniel Colascione, 2021/07/24
- Re: [SPAM UNSURE] Re: [SPAM UNSURE] Re: Tree Sitter (was Re: cc-mode fontification feels random), Stephen Leake, 2021/07/26
- Re: [SPAM UNSURE] Re: Tree Sitter (was Re: cc-mode fontification feels random), Perry E. Metzger, 2021/07/25
- Re: Tree Sitter (was Re: cc-mode fontification feels random), Perry E. Metzger, 2021/07/22
- Re: Tree Sitter (was Re: cc-mode fontification feels random), Richard Stallman, 2021/07/23
- Re: Tree Sitter (was Re: cc-mode fontification feels random), Stephen Leake, 2021/07/25
- Ada (was Re: Tree Sitter), Perry E. Metzger, 2021/07/25
- Re: Ada (was Re: Tree Sitter),
Stephen Leake <=
- Re: Ada (was Re: Tree Sitter), Stephen Leake, 2021/07/26
- Re: Ada (was Re: Tree Sitter), Perry E. Metzger, 2021/07/26
- Re: Ada (was Re: Tree Sitter), Perry E. Metzger, 2021/07/26
- Re: Ada (was Re: Tree Sitter), Richard Stallman, 2021/07/26
- Re: Ada (was Re: Tree Sitter), Perry E. Metzger, 2021/07/27
- Re: Tree Sitter (was Re: cc-mode fontification feels random), John Yates, 2021/07/25
- Re: Tree Sitter (was Re: cc-mode fontification feels random), Stephen Leake, 2021/07/24
- OFF-TOPIC: Ada availability (was: Tree Sitter), Óscar Fuentes, 2021/07/24
- Re: OFF-TOPIC: Ada availability (was: Tree Sitter), tomas, 2021/07/25