←back to thread

Introduction to Ada: a project-based exploration with rosettas

(blog.adacore.com)
193 points jaypatelani | 4 comments | 02 Sep 25 17:32 UTC | HN request time: 0.85s | source
Show context
giancarlostoro ◴[02 Sep 25 18:15 UTC] No.45106948[source]▶
So is there a list or statistic of how many DOD projects actually use Ada?
replies(4): >>45107636 #>>45108324 #>>45108359 #>>45111087 #
1. inamberclad ◴[02 Sep 25 20:10 UTC] No.45108359[source]▶
Nvidia is notably using Ada for serval modern projects.
replies(1): >>45108806 #
2. tos1 ◴[02 Sep 25 20:45 UTC] No.45108806[source]▶
I’m interested. Do you have a link or can you elaborate?
replies(1): >>45109484 #
3. sillywalk ◴[02 Sep 25 21:44 UTC] No.45109484[source]▶
Looks like they're using the SPARK subset of Ada:

"NVIDIA began implementing SPARK in its security strategy in 2019 on select pieces of firmware. They began training additional personnel in SPARK and eventually developed an in-house training program.

Several NVIDIA teams are now using SPARK for a wide range of applications that include image authentication and integrity checks for the overall GPU firmware image, BootROM and secure monitor firmware, and formally verified components of an isolation kernel for an embedded operating system, to name just a few."[0]

https://www.adacore.com/nvidia

[0] https://www.wevolver.com/article/nvidia-adoption-of-spark-us...

replies(1): >>45112502 #
4. cpeterso ◴[03 Sep 25 05:30 UTC] No.45112502{3}[source]▶
Here’s a related talk: “NVIDIA - Securing the Future of Safety and Security of Embedded Software”

https://youtu.be/2YoPoNx3L5E

> 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.