[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Ada (was Re: Tree Sitter)

From: Perry E. Metzger
Subject: Ada (was Re: Tree Sitter)
Date: Sun, 25 Jul 2021 15:52:51 -0400
User-agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.15; rv:91.0) Gecko/20100101 Thunderbird/91.0

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

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

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.


reply via email to

[Prev in Thread] Current Thread [Next in Thread]