Learning to Love a Rigid and Inflexible Language
I am old enough to remember the publication of the Strawman, Woodenman, Tinman, Ironman, and Steelman specifications for a new computer language in the mid 1970s — the language that became Ada. A few years later I read C. A. R. Hoare's Turing Award speech where, after criticizing the complexity of ALGOL 68, he turned his withering gaze on the new Ada language:
Do not allow this language in its present state to be used in applications where reliability is critical.... The next rocket to go astray as a result of a programming language error … may be a nuclear warhead exploding over one of our own cities. An unreliable programming language generating unreliable programs constitutes a far greater risk to our environment and to our society than unsafe cars, toxic pesticides, or accidents at nuclear power stations.
Having delighted in Hoare’s speech, particularly the fable at the end about the clothes that had no emperor, I overlooked Hoare's later support for Ada. That is, until a few years ago my view of Ada as a programming language was clear: an inflated, inflexible language useful only in a few legacy military applications, of no use to anyone working with high-performance embedded code.
Meeting Ada
Until the COVID-19 virus appeared, I used to attend the annual Safety Critical Systems Symposium in the UK in person. A company called AdaCore always had a stand at that symposium, and a few Februarys ago I chatted with their representative during a break. My opening Dunning and Kruger gambit was along the lines of “I work with high-performance, embedded software, so what you have to offer with Ada is obviously of no use to me”. I may even have ended that with a chuckle.
Her response was a simple challenge: “When did you last look at Ada?”
Confessing that my only look at Ada had been very superficial and some 35 years previously, I was given Quentin Ochem's Ada for the C++ or Java Developer, and John McCormick and Peter Chapin's Building High Integrity Applications with SPARK. I read these on the flight back to Canada and, arriving home, experimented with a simple program. The result was enough to put me off Ada for life. I tried to write a “Hello World” program:
with Ada.Text_IO; use Ada.Text_IO;
procedure Main is
MyString : String(1 .. 20);
begin
MyString := "Hello World";
Put_Line(MyString);
end Main;
The compiler gave me a warning which, of course, I ignored — real programmers don’t read compiler warnings. When I ran the program, this appeared:
raised CONSTRAINT_ERROR : main.adb:6 length check failed
My first thought was that I had tried to copy too many characters into MyString and that unlike C's strcpy() Ada’s compiler had caught my error. But “Hello World” has only 11 characters, certainly fewer than 20. This was Ada’s strong typing kicking in: “Hello World” is not a 20-character string, and so it cannot be put into MyString.
Falling for Ada
Working in the world of safety-critical, embedded systems, I was spending a lot of time trying to avoid the pitfalls of the C language: I realised that the teams of people working to define the MISRA-C and SEI CERT C subsets of C were trying to reduce the C language to a safer subset. I was familiar with the supposedly safe subsets of D and Rust, and following the interesting results of my “Hello World” experiment, I thought the time had come for me look seriously at Ada again, and in particular, the SPARK subset.
I bought John Barnes’ formidable (949 pages) Programming in Ada 2012 and, while I didn’t read it cover-to-cover, I started creating programs larger than my first Hello World. Like other programmers who’ve commented to me about Ada, I was exasperated with the compiler—until I came to appreciate that it was protecting me from myself. I also came to realise that Ada is not the dead language I had assumed, not a failed enterprise whose development had stopped in the early 1980s. At the time of writing, the latest versions are Ada 2012 and SPARK 2014, sufficiently recent to be useful today, and not so recent as to be untried.
The SPARK subset of Ada allows the correct operation of a program to be proven statically. This capability completed my awakening and brought me to embrace Ada. This occurred when I prepared a small SPARK example for a programming class I was teaching. My intention for this class had been to:
- Write a simple program.
- Test the program to ensure it was correct.
- Run the SPARK prover to prove the program was correct.
- Insert a minor bug.
- Run the prover again to demonstrate to the class that the SPARK prover could detect the bug.
My program performed a simple calculation, very inefficiently, to find the smallest factor of an integer. It returned the smallest factor and the “other” factor:
procedure SmallestFactor (N : in out Positive; Factor : out Positive)
with
Post => (N = N'Old / Factor) and (N'Old rem Factor = 0) and
(for all J in 2 .. Factor - 1 => N'Old rem J /= 0);
For example, calling SmallestFactor (N, F) with N = 245489 should return N = 31 as the smallest factor and F = 7919 as the “other” factor.
Steps 1 and 2 went well. I wrote the program and tested it with numerous suitable inputs (e.g., 245489) and found it worked correctly—or so it seemed. It was at Step 3 that my eyes were opened. The SPARK prover told me that my program was incorrect; if the input is 9, then the program gives erroneous output:
cannot prove N = N’Old / Factor
e.g. when Factor = 1 and N = 3 and N’Old = 9
I didn’t need to insert the minor bug! I had inserted it inadvertently, and I had not found it during testing. The program works perfectly for any input value other than 9. Thanks to Ada and SPARK, I had a far better teaching example than the one I had tried to create.
While I was belatedly getting to know Ada, AdaCore popped up again when a joint BlackBerry QNX and AdaCore customer wanted to use Ada. With my new-found enthusiasm, I became one of the BlackBerry QNX contacts with AdaCore. For some years now the AdaCore compiler and libraries have been available on BlackBerry® QNX® systems.
Today
As I write this, I have a serious Ada program consisting of 19 source code files containing 2,985 comment lines and 6,253 of Ada code open on my desktop. This forms part of a semi-formal verification suite of a new QNX development in progress at the moment. In the past I would have written this program in C or Python. Writing it in Ada has sometimes been infuriating because I turn on all compiler warnings and specify that warnings are to be treated as errors. However, Ada’s characteristics have saved me hours of debugging. Getting a clean compilation takes a little longer, but that is more than compensated by the reduced debugging effort.
On several occasions I have needed help and have found excellent help from the Ada group at StackOverflow and from the AdaCore support desk. My questions have ranged from “what is the more Ada-ish way of doing this?”, to deep questions about race conditions between tasks (the Ada term for “threads”). Answers both from StackOverflow and AdaCore support have always been prompt, professional and polite.
Embracing Ada
I very much like a great deal of Ada's syntactic sugar, for example, being able to break up long integers and floating point values for improved human readability:
IndiaPopulation : constant Positive := 1_352_642_280;
However, it is Ada’s semantics that are obviously most important. Working with highly-threaded, embedded code, I particularly like Ada’s concept of a “protected variable”, a variable to which access is limited to one thread (“task” in Ada-speak) at a time, and the related support for protected shared buffers used between tasks.
Apart from very short, run-once programs, I must confess that Ada is now my language of choice. I am getting a lot of use out of our Ada compiler.
About Chris Hobbs
Chris Hobbs is the author of the definitive book on functional safety, Embedded Software Development for Safety-Critical Systems. He has advised some of the largest industrial control and automotive companies as they pursued safety-certification standards.
