AdaCore
1 HN recommender · recommended in 5 months, 2022–2026
58:37 · 5K views · Nov 10, 2020
An AdaCore webinar in which NVIDIA engineers explain why and how they adopted Ada and SPARK for security-critical firmware. It covers the business case and the engineering experience of the transition.
HN cites it in Rust-versus-C++ and Ada discussions as a real industrial case of choosing SPARK for safer embedded code.
7 comments from Hacker News
Author of the book here, thank you for your feedback! Though not an Ada expert, I have used the SPARK subset. And I’ve worked on security assessment of military systems with components written in Ada. Although we looked at binaries and not source code, because our assurance model did not consider the Ada compiler to be part of the chain of trust (so we test the artifact the CPU will execute). I really like Ada and hope to use more of it in the future! The HN community may be interested in this 1 hour presentation [1] on Nvidia's adoption of Ada, including why they chose it over Rust in 2019 (regulatory certification was one factor). There’s also a great academic paper [2] on the recent advances SPARK has made in heap memory verification, inspired in part by Rust’s type system. There are currently efforts underway to certify Rust for usage in safety critical systems via an alternate, certified toolchain (among other pieces of the puzzle). Two related initiatives are linked through in FAQ question #7 (which someone already shared). I’ll be sure to add the Ferrous Systems and AdaCore collaboration when I have a chance to batch together some updates. I, like many others, believe Rust is a technology that can deliver value in safety and mission critical verticals due to reduction in undefined behavior via principled static analysis (a type system for which there has been early success in formal verification of safety claims[3]). Looking forward to digging into Rust research tools
Ada offers security and simplicity and is already part of GCC but also has llvm now. Linux kernel drivers have also been demonstrated. Perhaps it would be healthier for Rust to have competition? [LINK] [LINK] [LINK] Nvidia also chose Spark; a built in subset of Ada as being more cost effective for secure code than C++. this video Assembly is also supported by Ada and I found it far easier to add than with C even. C interface support is also excellent.
Ada offers security and simplicity and is already part of GCC but also has llvm now. Linux kernel drivers have also been demonstrated. Perhaps it would be healthier for Rust to have competition? [LINK] [LINK] [LINK] Nvidia also chose Spark; a built in subset of Ada as being more cost effective for secure code than C++. this video Assembly is also supported by Ada and I found it far easier to add than with C even. C interface support is also excellent.
Ada offers security and simplicity and is already part of GCC but also has llvm now. Linux kernel drivers have also been demonstrated. Perhaps it would be healthier for Rust to have competition? [LINK] [LINK] [LINK] Nvidia also chose Spark; a built in subset of Ada as being more cost effective for secure code than C++. this video Assembly is also supported by Ada and I found it far easier to add than with C even. C interface support is also excellent.
Here’s a related talk: “NVIDIA - Securing the Future of Safety and Security of Embedded Software” this video > NVIDIA is working with AdaCore to implement Ada and SPARK programming languages into certain firmware elements to reduce this potential error. In this webinar you will learn how the combination of NVIDIA hardware with Ada and SPARK delivers robustness and security, improving efficiency and safety in the development pipeline.