Re: Ada (was Re: Tree Sitter)

[Stephen Leake]

"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