Недавно AdaCore, компания, владеющая известными языками программирования Ada и SPARK, заявила, что продукты NVIDIA используют большое количество формально проверенного кода SPARK. Для более чувствительных к безопасности приложений или компонентов команда безопасности NVIDIA заменяет язык C на SPARK…
