有没有可证明的现实世界语言？（斯卡拉？）

Question

我在大学里被教过关于正规系统的知识，但是令我失望的是，它们似乎并没有被真正的单词使用。

我喜欢这样的想法：能够知道某些代码（对象，函数，任何东西）起作用，而不是通过测试，而是通过 证明 。

我确定我们都熟悉物理工程和软件工程之间不存在的相似之处（钢铁的行为可预测，软件可以做任何事情-
谁知道！），我很想知道是否有任何语言可以可以用真实的词来使用（是否要求太多Web框架？）

我听说过有关诸如scala之类的功能语言的可测试性的有趣事情。

作为软件 工程师 ，我们有哪些选择？

Answer 1

是的，有些语言旨在编写可证明正确的软件。有些甚至用于工业。Spark
Ada
可能是最突出的例子。我已经与Praxis
Critical Systems
Limited的一些人进行了交谈，他们将其用于在Boings上运行的代码（用于引擎监视），这看起来非常不错。（以下是该语言的精彩摘要/说明。）此语言及其随附的证明系统使用下面描述的第二种技术。它甚至不支持动态内存分配！

我的印象和经验是，有两种技术可以编写正确的软件：

• 技术1：用您喜欢的语言（例如C，C ++或Java）编写软件。采取这种语言的正式规范，并证明您的程序正确。

如果您的目标是100％正确（这在汽车/航空航天业通常是必需的），那么您将花费很少的时间进行编程，而花费更多的时间进行证明。

• 技术2：以一种稍显笨拙的语言（例如，Ada的某些子集或OCaml的调整版本）编写软件，并在编写过程中编写正确性证明。在这里编程和验证是齐头并进的。在Coq中编程甚至完全等同于它们！（请参阅库里-霍华德书信）

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

请注意，这两种方法都取决于您手头有一个正式的规范（您将如何分辨正确/不正确的行为）以及该语言的形式化语义（您将如何分辨实际的行为）您的程序是）。

这是正式方法的更多示例。是否是“真实世界”，取决于您问的人:-)

• Coq定理证明：用Coq编程（技术2）
• ESC / Java（技术1，虽然声音不完整）
• Spec＃（技术1，虽然声音不完整）
• Why / Krakatoa（技术2，基于Java）

我只知道一种“证明正确的” Web应用程序语言
：UR。确保“经过编译器”的Ur程序不会：

• 遭受任何形式的代码注入攻击
• 返回无效的HTML
• 包含无效的应用程序内链接
• HTML表单与其处理程序期望的字段之间不匹配
• 包括客户端代码，这些代码对远程Web服务器提供的“ AJAX”样式的服务做出了错误的假设
• 尝试无效的SQL查询
• 与SQL数据库或浏览器与Web服务器之间的通信使用不正确的封送或封送处理