Rust has plenty of attention as a low-level language that eliminates many of the errors which are easy to make in C, but according to a case study released by AdaCore and Nvidia, SPARK also merits attention.

Since AdaCore is SPARK’s main sponsor that is unsurprising but nevertheless shows that Rust is not the only choice for coders looking for better programming safety without compromising performance.

Nvidia is best known for its GPUs but is also involved in embedded systems, and writes firmware for the GPUs themselves. This is security-critical code. Principal software engineer Cameron Buschardt, who worked on replacing C with SPARK on new components, compared the SPARK modules with equivalents in C. “Looking at the assembly generated from SPARK, it was almost identical to that from the C code,” he said. “I did not see any performance difference at all. We proved all of our properties, so we didn’t need to enable runtime checks.”

NVIDIA has talked about this before. In 2019 robotics product manager Shri Sundaram, who was then responsible for car computers, said:

“SPARK, a subset of Ada, is able to mathematically prove whether code written in that language is error-free. This proof is able to define how the software application should behave. It also determines whether the implementation is in accordance with that definition, finding bugs or vulnerabilities that may not have been detected otherwise. By integrating these languages into NVIDIA hardware, the potential for the software to malfunction or be exploited is minimized.”

SPARK 2014 is the current version and is open source on GitHub, under the GPL-3.0 license. The project is led by AdaCore and primarily developed by AdaCore, Capgemini and Inria (a French national research institute). Development is slower than that of Rust, but this may be an advantage, and the paper cites that “Ada, SPARK’s basis, is a very mature language.”

It is well-known that Rust can be challenging to learn. SPARK may be easier, particularly for those familiar with embedded programming. Whereas Rust is focused on memory safety, SPARK is focused on proven correctness, a different approach that may be easier to grok.

All that said, the SPARK advocates look unlikely to disrupt the momentum behind Rust, not least because of Rust’s emerging support in the Linux kernel.