back

by jasonpeacock·1y ago·view on hn ↗
They used SPARK instead:

  SPARK is a formally defined computer programming language based on the Ada programming language,
  intended for the development of high integrity software used in systems where predictable and
  highly reliable operation is essential. It facilitates the development of applications that demand
  safety, security, or business integrity.
https://en.wikipedia.org/wiki/SPARK_(programming_language)
4 comments
People who don't want to read the first line of the article, rejoice!

It sounds like a good decision though. Formal verification tends to make more sense in highly concurrent situations where there is a high-value stable API to be supported. That describes graphics cards and surrounding environments really well so it makes sense that Nvidia would find use cases.

Something more from the article is also that they made the decision with a pilot project that went well. It'd be nice to have more details about it; that sort of thing is important to do well and always interesting. Lo and behold, we do have more details about it! https://blog.adacore.com/when-formal-verification-with-spark... - there is a video in there that looks to be worth a watch.

Nothing in the article explained what SPARK is. I appreciated GP's comment.
I really wish there was more active development on SPARK.

It's largely untouched over the last 10-years.

https://github.com/AdaCore/spark2014

For those not aware, SPARK gives even more safeguards/guarantees than Rust (see below) ... and also does it at compile time (when not all of Rust safeguards are at compile time).

https://blog.adacore.com/should-i-choose-ada-spark-or-rust-o...

There's 27k commits. that's pretty active
They actually had to use the non-cutdown version of SPARK that this company sells, called SPARK Pro.
SPARK is free for all to use and is open source. They chose to pay for Adacores pro support services and verified pro Ada compiler over the FSF GCC/Gnat Ada compiler. Spark is actually part of the Gnat compiler (compatibility) but actually the slower analysis is done by gnatprove thereby keeping compilation and iterative development fast. Nvidia can certainly afford to do so of course.
AdaCore's pro support includes more recent releases and, in case of problems, wavefronts. That said, the free version is fairly recent, and you can get community (and sometimes vendor) support.
SPARK has some adherents in spacecraft programming for its formal verifiability and safety features.