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

【问题标题】：Programming Language Choices for High Integrity Systems高完整性系统的编程语言选择
【发布时间】：2026-01-03 01:45:02
【问题描述】：

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

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

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

编辑：高完整性系统是安全关键系统等、安全系统等的总称。

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

【问题讨论】：

【解决方案1】：

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

SPARK 可以在没有运行时的情况下使用。对于 Ada 语言也是如此（参见 pragma No_Runtime）。

当然，对于 SPARK 等语言，您是在用灵活性换取安全性（或安全性）。

【讨论】：

【解决方案2】：

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

【讨论】：

【解决方案3】：

您需要多高的诚信度？

俄勒冈州波特兰市的Galois 在Haskell 编写的高完整性系统上建立了非常成功的业务。我相信他们强调数据的完整性和安全性。用如此复杂的语言、非常复杂的运行时系统来做这种工作有点令人惊讶，但是 Haskell 的类型系统提供了非常强大的保证，并且语言语义提供了比大多数语言强得多的推理原理。此外，您倾向于为每个应用程序编写更少的代码，因此很容易显示正确。
如果您需要更强大的保证，SPARK Ada（或者现在只是 SPARK）是一种相对简单的传统命令式语言，它带有完整的形式语义和用于完整形式验证的工具。与使用 Haskell 相比，您可以获得更强大的保证，但在资本和劳动力方面的价格要高得多。

【讨论】：

【解决方案4】：

您可能想从Eiffel 的角度来思考，其中更强大的前置条件和后置条件的执行使高完整性系统更容易。

【讨论】：

【解决方案5】：

这在术语上是矛盾的。强类型、块结构的语言几乎总是由编译器编译，产生程序员不负责的机器代码。如果你想对代码100%负责，你需要使用汇编语言。

【讨论】：

【解决方案6】：

我不完全理解什么是“高完整性系统”。假设您的意思是“一个为 bug 留下较少空间的系统”，我建议您看一下 ML，它是 OOP 的派生词，O'CaML。 ML 旨在最大限度地减少类型错误。 ML 中没有转换错误或空指针 - 您根本无法对其进行编码。它还缺乏动态功能 - 这使得它不那么酷但更安全。

话虽如此，ML 远非黑客的乐趣；这是一种有些繁琐的语言。但是，如果您希望多工作一个小时而少获得一个例外，那么这是一个相关的选择。

【讨论】：

【解决方案7】：

你可能会寻找你想要的东西，但你不会得到它。

您的要求彼此不兼容。他们基本上完全排除了任何类型的图书馆。你可以说你可以使用 C / C++ - 但没有任何包含文件和标准库（程序员显然不会对此负责）。

这使您几乎处于旱地 - 要求是不切实际的。即使有一个庞大的团队，也不希望对大多数库进行重新编程。

如果你有适当的编程方法，Java 实际上是相当不错的——而且足够有趣的是你的要求（高完整性系统）更多的是编程方法的问题（单元测试、大量内部测试、多个实例并行比较结果——比如航天飞机控制计算机——万一发生故障）而不是语言决定的。

【讨论】：