Ada (was Re: Tree Sitter)

[Perry E. Metzger]

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.

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