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