高完整性系统的编程语言选择

Question

哪些编程语言是高完整性系统的不错选择？

糟糕选择的一个例子是Java,因为程序员无法访问大量代码.我正在寻找强类型块结构语言的例子,其中程序员负责100%的代码,并且尽可能少地受到JVM之类的干扰.

编译器显然是一个问题.语言必须有完整而明确的定义.

编辑:高完整性系统是安全关键系统等,安全系统等的总称.

编辑编辑:我想要不受平台影响的语言示例,无论编译器如何,都会产生相同的结果,并且是完全定义的.

Answer 1

我认为 ADA 通常用于此目的。

Answer 2

Ada 的 SPARK 子集将是一个非常好的起点。SPARK 继承了 Ada 的所有优良特性（强类型、易于阅读……），并具有没有未定义特性的额外好处，这意味着所有 SPARK 程序都会执行完全相同的操作，无论使用哪种 Ada 编译器编译它。

SPARK 可以在没有运行时的情况下使用。Ada 语言也类似（请参阅 pragma No_Runtime）。

当然，对于 SPARK 等语言，您需要用灵活性来换取安全性（或保障）。

Answer 3

您寻求多高的诚信度？

• 俄勒冈州波特兰市的Galois在用Haskell编写的高完整性系统上建立了非常成功的业务。我相信他们强调数据完整性和安全性。用如此复杂的语言、非常复杂的运行时系统来完成这种工作有些令人惊讶，但 Haskell 的类型系统提供了非常强大的保证，并且语言语义提供了比大多数语言更强的推理原理。此外，您倾向于为每个应用程序编写更少的代码，因此很容易显示正确性。

• 如果您需要更强的保证，SPARK Ada（或者现在只是 SPARK）是一种相对简单的传统命令式语言，带有完整的形式语义和用于完整形式验证的工具。你会得到比 Haskell 更强的保证，但资本和劳动力的价格要高得多。