4 ms·

They used SPARK instead: SPARK is a formally defined computer programming language based on the Ada programming language, intended for the development of h

• roenxi 2y ago
  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-is-the-strongest-link https://blog.adacore.com/when-formal-verification-with-spark... - there is a video in there that looks to be worth a watch.
  • MichaelDickens 2y ago
    Nothing in the article explained what SPARK is. I appreciated GP's comment.
• rs186 2y ago
  [flagged]
  • Tadpole9181 2y ago
    I'm with you in spirit, but NVIDIA Spark is a thing insofar as RAPIDS? https://www.nvidia.com/en-us/deep-learning-ai/solutions/data-science/apache-spark-3/ https://www.nvidia.com/en-us/deep-learning-ai/solutions/data...
    • antonvs 2y ago
      Yes, but that has nothing to do with the Spark language that Nvidia is talking about in the OP: https://en.wikipedia.org/wiki/SPARK_(programming_language) https://en.wikipedia.org/wiki/SPARK_(programming_language) Seems like a great example of LLMs getting confused by language and lacking any actual understanding, although I haven't yet looked into this particular case.
      • rs186 2y ago
        And Nvidia never used the term "NVIDIA Spark". In fact those words probably never appeared together on the Internet.
• RachelF 2y ago
  They actually had to use the non-cutdown version of SPARK that this company sells, called SPARK Pro.
  • kevlar700 2y ago
    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.
    • simon4ada 2y ago
      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.
      • SkyMarshal 2y ago
        What are wavefronts? Not getting many search results on that, besides a few github issues mentioning them. https://github.com/AdaCore/RecordFlux/issues/955 https://github.com/AdaCore/RecordFlux/issues/955 https://learn.adacore.com/search.html?q=wavefront&check_keywords=yes&area=default https://learn.adacore.com/search.html?q=wavefront&check_keyw... (nada) https://docs.adacore.com/spark2014-docs/html/ug/search.html?q=wavefront&check_keywords=yes&area=default https://docs.adacore.com/spark2014-docs/html/ug/search.html?... (nada) https://github.com/AdaCore/spark2014/issues?q=wavefront%20 https://github.com/AdaCore/spark2014/issues?q=wavefront%20 (nada)
• alberth 2y ago
  I really wish there was more active development on SPARK. It's largely untouched over the last 10-years. https://github.com/AdaCore/spark2014 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-over-c-c https://blog.adacore.com/should-i-choose-ada-spark-or-rust-o...
  • nmz 2y ago
    There's 27k commits. that's pretty active
• mbonnet 2y ago
  SPARK has some adherents in spacecraft programming for its formal verifiability and safety features.