[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
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
- Re: Tree Sitter (was Re: cc-mode fontification feels random), (continued)
- Re: Tree Sitter (was Re: cc-mode fontification feels random), Daniel Colascione, 2021/07/21
- 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 <=
- Re: Ada (was Re: Tree Sitter), Stephen Leake, 2021/07/26
- 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