NVIDIA 尝试使用 SPARK 语言取代 C 语言

SPARK 是一种编程语言和一组验证工具，旨在满足高保证软件开发的需求。SPARK 基于 Ada 语言，它既对 ada 语言进行子集化以删除无法验证的功能，又扩展了合约和方面的系统，进一步支持模块化、形式化验证。SPARK 语言一般用于可预测和高度可靠操作的系统中的高完整性软件，它有助于开发需要高安全性或业务完整性的应用程序。