Ada 的主要特点是类型安全，可读性好。Ada 95 是第一个标准化的面向对象语言。Ada 2012 加入了 design by contract. SPARK 是 Ada 的可形式验证的子集，可以利用 Z3, CVC4 等形式验证工具证明程序不会崩溃。

关于 NVIDIA 使用 Ada 语言的资料：

https://blogs.nvidia.com/blog/2019/02/05/adacore-secure-autonomous-driving/
https://blog.adacore.com/when-the-isa-is-the-weakest-link

【 在 hgoldfish (老鱼) 的大作中提到: 】
: 是不是因为这个语言比较简单，比较自洽。适合写严肃的业务脚本。
--
FROM 103.90.178.*

费劲黑半天，要卖钱的吧

这18G里面已经有不少东西了

【 在 verilog 的大作中提到: 】
: 不是说75G吗？这个只有18.9G
--
FROM 114.241.225.*

linux 不用抱怨nvidia不给源代码了。
：）

【 在 xunery 的大作中提到: 】
: 新闻报的，压缩包18.8g，解压后75g
--
FROM 117.147.23.*

ada这个优点适合驱动，那内核是不是也适合？
【 在 ArchLinux (a lightweight and flexible distribution) 的大作中提到: 】
: Ada 的主要特点是类型安全，可读性好。Ada 95 是第一个标准化的面向对象语言。Ada 2012 加入了 design by contract. SPARK 是 Ada 的可形式验证的子集，可以利用 Z3, CVC4 等形式验证工具证明程序不会崩溃。
: 关于 NVIDIA 使用 Ada 语言的资料：
: https://blogs.nvidia.com/blog/2019/02/05/adacore-secure-autonomous-driving/
: ...................
--
FROM 114.249.17.*

喔！Ada/Spark 泪流满面，我比 Rust 更安全，更易读，更高效，更强大，快来看看我啊～

【 在 ArchLinux 的大作中提到: 】
: 之前看到一些资料说 NVIDIA 在使用 Ada/SPARK 语言写一些 RISC-V 的软件，看了压缩包里面 nvriscv 里面有不少 *.ads, *.adb 文件，应该证实了这个说法。
:
--
FROM 124.64.120.*