Why not use SPARKAda?

Question

Beyond some valid reasons not to use a new tool such as support of legacy code, no in-house SPARKAda knowledge base, why hasn't SPARKAda caught on? It seems like a very sound tool for many projects requiring high reliability, so I don't understand why its not so common. I would be more comfortable knowing that the avionics software that powers my flight was developed using a programming language that lends itself to verifiability techniques as suppose to being written in the C language.

Answer 1

I just saw the slashdot post about the new open source project using SPARK Ada. It's a chicken and the egg phenomenon really because a language has to be have a big project that champions it (usually in the open source community) before it can become big. But of course a language must be sufficiently widespread for a big open source project to utilize it. So now that there are some high profile open source projects coming out in SPARK it may become a more popular language.

Case and point: think about how big Ruby was before Rails, and how big it got after Rails.

Answer 2

It doesn't really offer a lot to mainstream development projects. IMO these would be the main reasons:

• The hard part of high reliability systems is not the language but the methodology. SPARK has features to support static verification but most people don't really have the skill to use this.

• The language has relatively little mature library support of the sort afforded by more widely used platforms such as Python, .Net or C++ so it's starting from behind.

• Ada is regarded as a bit of a bondage-and-discipline language so it's never developed much of a hacker community.

• High reliability systems are time consuming and expensive to build so there not always a business case to use that sort of methodology. If you are not in the business of building safety-critical or other high reliability systems SPARK or ADA do not have much to offer.

EDIT: See this Stackoverflow post for a discussion about safety-critical software.

Answer 3

Also, another important reason that wasn't yet really mentioned: it is just since pretty recently that a SPARK/Ada implementation is easily (freely) available, to quote wikipedia:

In early 2009, Praxis formed a partnership with AdaCore, and released "SPARK Pro" under the terms of the GPL. This was followed in June 2009 by the SPARK GPL Edition 2009, aimed at the FLOSS and academic communities.

In other words, you can now actually download a GPL version of SPARK/Ada:

SPARK GPL Edition 2009 Edition Now Available!

SPARK Pro provides the foremost language, toolset and design discipline for the engineering of high-assurance software. It combines the renowned SPARK language and verification tools from Praxis with the GNAT Programming Studio (GPS) and GNATBench development environments from AdaCore.

This release includes:

• Complete SPARK language and toolset, including RavenSPARK and Proof Checker.
• Significant improvement in both performance and completeness of the Simplifier over any previous release.
• Integration with GPS 4.3.1 and GNATBench 2.3.0 and above.
• Availability of full sources for all the tools. The SPARK GPL Edition is available on Windows, SPARC/Solaris, Linux (both 32- and 64-bit) and Apple’s OS X (64-bit).

AdaCore and Praxis are dedicated to developing the finest tools available for software development with SPARK and Ada. The SPARK GPL Edition is the development environment for Free Software development and the GNAT Academic Program for use in Academia. SPARK Pro is for commercial/industrial development.

• AdaCore libre
• The SPARK Pro Package

Answer 4

Using SPARK-Ada on a project requires, like most critical systems development, dedication to a mindset, a methodology, and a tool. Unfortunately, the latter is the only facet that a typical industry team has in spades. ("We are a Java house.")

Consequently, it isn't about development teams not choosing to use SPARK-Ada, it is about teams simply being unable to use SPARK-Ada.

If you are performing critical systems development, you have only a few choices when it comes to professionally supported industrial-grade tools. Praxis is second-to-none in this regard.

Answer 5

I have just started work in Avionics embedded systems. In our company SPARK is the tool of choice - along with loads of procedures and a mind-numbing amount of paperwork. I think you can rest a little easier when boarding the next plane. Car controllers on the other hand are developed mostly using a subset of C. So applying the breaks early in the wet is advised :)