SPARK started in 1987 as a restricted subset of Ada 83, defined by its own grammar rules. The overhaul of the language and toolset starting in 2010 increased greatly the language subset, dropping in effect the need for separate grammar rules. Since then, SPARK has progressively adopted most of the Ada features, to a point where the last remaining non-SPARK significant Ada feature today is pointers. We have started work on including safe pointers in SPARK, borrowing the ideas of pointer ownership from Rust. So one can legitimately wonder what difference remains between SPARK and Ada.
In the first part of this talk, I will lay out the principles that have guided us through the inclusion of language features in SPARK since 2010. I will describe in particular the trade-offs that we considered for support of important features like recursion, types with non-static constraints, generics, object orientation, concurrency. I will give a preview of the support envisioned for pointers in SPARK. So that the distinction between Ada and SPARK appears clearly: it's not about quantity, it's about safety and security.
In the second part of this talk, I will give a tour of FOSS projects which are using SPARK today: Aida, Certyflie, Muen, PolyORB-HI, Pulsar, StratoX, Tokeneer. For each one, I will describe at which level of assurance SPARK is used, with how much efforts and for which benefits. Then I will focus on the largest one, Muen, an x86/64 separation kernel for high assurance. Finally, we will look at the resources which are available to the community for FOSS development in SPARK.
Speakers: Yannick Moy