Re: Ada (was Re: Tree Sitter)

["Perry E. Metzger" <perry@piermont.com>]

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:
> https://github.com/tree-sitter/tree-sitter/issues/693

Thank you for reporting that.


Perry