[Top][All Lists]

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

Re: Ada (was Re: Tree Sitter)

From: Perry E. Metzger
Subject: Re: Ada (was Re: Tree Sitter)
Date: Mon, 26 Jul 2021 09:45:40 -0400
User-agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.15; rv:91.0) Gecko/20100101 Thunderbird/91.0

On 7/26/21 01:05, Stephen Leake wrote:
"Perry E. Metzger" <perry@piermont.com> writes:

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.

I'm sure that improvements are being worked on, but the state of the art in language design really has moved on. No version of Ada has affine types, and no version of Ada _could_ get affine types without breaking the entire existing codebase.

It's not easy to retrofit it to the language without completely altering the language. If you start working in a language with linear or affine types you will immediately see why.

I agree that strongly typed languages with detection of array bounds violations and other undefined behavior are superior. Your own experience is evidence for that. You got lots of years of good work done in Ada that would not have been as easy in languages like C or C++. I agree those languages are full of traps for the unwary. I do not think, however, that Ada is the best choice for any new project being undertaken today. As I said, the state of the art has advanced dramatically in 40 years.

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 think you should try it anyway. At very worst, you will learn a great deal. You might also produce a library of interest to other people, and I think having more tools of this sort in the world is better.

That said, I think for good or ill, the current iteration of Emacs works best with code written in C. That might eventually change, of course. Even the Linux kernel is now getting support for code written in Rust. Perhaps eventually, with the arrival of better and better versions of the Rust GCC front end and other tools, it will make sense for Emacs to have a mixed implementation. I don't think that time has arrived yet.

(BTW, note that Tree Sitter is not written in Rust, though it does have a Rust API 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 :).

For now, but if I had to write a small high assurance real time kernel at the moment, I'd probably write it in a little language embedded in straight Coq with extraction to something with an efficient compiler (like Rust) even if the extraction wasn't verified.

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:

Thank you for reporting that.


reply via email to

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