java - 是否有任何可证明的现实世界语言？ (斯卡拉？)

Question

我被教导了 formal systems在大学时，但我很失望他们似乎并没有被真正使用。

我喜欢能够知道某些代码(对象、函数等)是否有效的想法，而不是通过测试，而是通过证明。

我相信我们都熟悉物理工程和软件工程之间不存在的相似之处(钢的行为可预测，软件可以做任何事情 - 谁知道呢!)，我很想知道是否存在任何可以在现实世界中使用的语言(对 Web 框架的要求太多了吗？)

我听说过有关 scala 等函数式语言的可测试性的有趣事情。

作为软件工程师我们有什么选择？

Answer 1

是的，有些语言专为编写可证明正确的软件而设计。有些甚至用于工业。 Spark Ada可能是最突出的例子。我与 Praxis Critical Systems Limited 的一些人交谈过，他们将它用于在 Boings 上运行的代码(用于引擎监控)，它看起来相当不错。 (这里有一个很棒的summary / description of the language。)这种语言和随附的证明系统使用下面描述的第二种技术。它甚至不支持动态内存分配!

---

我的印象和经验是编写正确的软件有两种技巧:

• 技巧 1:用您熟悉的语言(例如 C、C++ 或 Java)编写软件。采用这种语言的正式规范，并证明您的程序是正确的。

  如果您的目标是 100% 正确(这通常是汽车/航空航天行业的要求)，那么您将花费很少的时间进行编程，而将更多的时间用于证明。

• 技巧 2:用稍微笨拙的语言编写软件(例如 Ada 的某个子集或 OCaml 的调整版本)，并在此过程中编写正确性证明。在这里，编程和证明齐头并进。 Coq 中的编程甚至完全等同于它们! (见Curry-Howard correspondence)

  在这些情况下，您总是会得到一个正确的程序。 (一个错误将被保证 Root 于规范中。)您可能会花更多时间在编程上，但另一方面，您会在此过程中证明它是正确的。

请注意，这两种方法都取决于您手头有一个正式的规范(否则您将如何判断什么是正确/不正确的行为)和一个正式定义的语言语义(否则您将如何判断你的程序的实际行为是)。

这里还有一些正式方法的示例。如果它是“真实世界”，取决于你问谁:-)

• Coq 定理证明器:Programming with Coq (技巧2)
• ESC/Java (技巧一，虽然不完善也不完整)
• Spec# (技巧一，虽然不完善也不完整)
• Why / Krakatoa (技术 2，基于 Java)

我只知道一种“可证明是正确的”网络应用程序语言:UR .保证“通过编译器”的 Ur 程序不会:

• 遭受任何类型的代码注入(inject)攻击
• 返回无效的 HTML
• 包含无效的应用内链接
• HTML 表单与其处理程序预期的字段不匹配
• 包含对远程 Web 服务器提供的“AJAX”样式服务做出错误假设的客户端代码
• 尝试无效的 SQL 查询
• 在与 SQL 数据库或浏览器和 Web 服务器之间的通信中使用不正确的编码或解码