Ada

I mentioned in a previous post that the Ada language and Gnat compiler added some very interesting features lately, like good ARM64 support and (for the SPARK subset) dependent typing. I live in Europe, which has definitely underemphasised military defense but that may change, and this post has a Franco-British bias, e.g. for companies. I studied Ada83 a long time ago in college, so decided to see what had changed in the intervening decades.

In case anyone is wondering, "why Ada", back in the 1980s it was a requirement for US DoD projects. That mandate was rescinded, but it's still specified by NATO STANAG (Standardisation Agreement) 3912 for avionics systems. Although it might have started in the US, a major compiler vendor now is French, and it has been taught in a lot of European universities. And I personally think it is a fine choice even outside its traditional domain. I've heard this "traditional domain" sometimes euphemised as "life-critical systems", where it's absolutely required to save (or take) a human life.

So since 1983 there have been several language revisions, the latest version is from 2022. A lot has changed, but the foundation was solid to begin with which helps a lot. Salient additions I noticed are object-orientation, a container class library (and many others), and something I'm interested in, a subset called SPARK that supports static analysis using theorem provers.

Development Environment Setup

It's an ISO language, there are multiple vendors, but I'd recommend only one way. Install Alire. If you're on ARM macOS, you'll need to install a different compiler toolchain first and tell Alire to use it (this is easy). A similar platform-specific note, the ARM64 Linux version (which I wanted for a server) is built on Ubuntu so probably works best there (Ubuntu, of course, is a British distro).

Alire, a toolchain and library manager

A better toolchain for ARM64 macOS

For a text editor, I'd recommend Emacs. There's a very nice post on setting this up for Ada development.

Setting up Emacs for Ada

You'd have to check any libraries you link, but at least the core tools above are all licensed with the GCC runtime exception, so could be used for commercial purposes. If you earn a lot of money, paying AdaCore (who contribute to a lot of the above) for a license probably makes sense.

AdaCore

Getting Started Writing Software

The tooling support is good, but like any language things are done differently so you have to learn at least a little. For example, a tool called gprbuild is used instead of make, but it works fine. If you follow the Alire tutorials you won't go far wrong.

It's not really a "getting started" thing, but I was interested so looked into the basics of using SPARK too:

1. Non-SPARK code can call SPARK code, but not the other way around, so you'll need to split some of your app into safe and unsafe parts.

2. Add "with SPARK_Mode => On" aspects to the .ads and .adb file for what should be the "safe code".

3. Run "gnatprove <file>" to run the theorem prover on it.

Libraries

If you don't feel like reinventing the wheel, I can recommend an "order of preference" for picking libraries:

1. Whatever AdaCore ship with their Gnat Pro product. This could be GtkAda for a GUI (I don't personally like the current fashion for Web tech like Electron GUIs). AUnit for a test harness, GnatDoc for documentation generation, etc. Notably, these are installable from Alire without paying for support (but please check the licensing).

Gnat Pro documentation, freely available even if you don't have a license

2. The intersection of the Awesome Ada list and whatever is in Alire. This seems a good filter to start with.

Awesome Ada list

3. Basically anything else. There is 40 years of software, and the older stuff can be found on ISO images from archive.org (see below).

Interesting Books & Software

Similar to what I found for Concurrent Logic Programming, archive.org has a good collection of books. I actually remember the 1st edition of Barnes, and Booch's "Software Engineering in Ada" started my weird obsession with trying to write software in a better way.

Archive.org's ada collection

Also, there were repositories of reusable software on the early Internet. The best source for this now is some ISO images, it's a nice history lesson and there are some gems in there. I might do a future post on this.

Public Ada Library

For something more topical, there's a nice flight controller package for a drone written in SPARK:

CertyFlie

Postscript

Oh, and by the way, although I broadly agree with 1st/2nd/3rd-wave feminism, Ms Lovelace may not be such a good role model. Yes, she wrote maybe the first programs but as far as I can tell it was because she had a massive gambling addiction and thought this would help win on the horses, there was no beautiful altruistic motive.

Back to my gemlog