有可证明的真实语言吗?(斯卡拉?)

是的,有些语言是为编写可证明正确的软件而设计的。有些甚至用于工业。 Spark Ada summary / description of the language )此语言和随附的证明系统使用下面描述的第二种技术。它甚至不支持动态内存分配!

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

• 技巧1:用你喜欢的语言编写软件(例如C、C++或java)。使用这种语言的正式规范,并证明您的程序是正确的。

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

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

下面是一些形式化方法的例子。是否是“现实世界”,取决于你问谁:-)

• Programming with Coq (技术2)
• ESC/Java (技术1,但既不健全也不完整)
• Spec#
• Why / Krakatoa

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

• 返回无效的HTML
• 包含死的应用程序内链接
• HTML表单与其处理程序期望的字段不匹配
• 包括对远程web服务器提供的“AJAX”风格的服务做出错误假设的客户端代码
• 在与SQL数据库或浏览器与web服务器之间的通信中使用不正确的封送处理或解组

为了回答这个问题,你真的需要定义你所说的“可证明”。正如Ricky指出的,任何类型系统语言都是一种内置证明系统的语言,每次编译程序时都会运行该系统。这些证明系统几乎总是令人遗憾的无能为力-回答诸如 String Int 避免问“名单排序了吗?”-但它们同样是证据系统。

不幸的是,你的证明目标越复杂,使用一个能检查你的证明的系统就越困难。当你考虑到图灵机器上不可判定的问题的绝对规模时,这种情况会很快升级为不可判定。当然,理论上你可以做一些基本的事情,比如证明你的排序算法的正确性,但除此之外的任何事情都将是无足轻重的。

即使要证明排序算法的正确性这样简单的事情,也需要一个相对复杂的证明系统。(注:由于我们已经建立了类型系统是语言中的一个证明系统,我将用类型理论来讨论,而不是更有力地挥动我的手)我相当肯定列表排序的完全正确的证明需要某种形式的依赖类型,否则你将无法在类型级别引用相对值。这立即开始进入类型理论的领域,这已经被证明是不可判定的。因此,虽然您可以证明列表排序算法的正确性,但唯一的方法是使用一个系统,该系统还允许您表达它无法验证的证明。就我个人而言,我觉得这很令人不安。

还有我前面提到的易用性方面。你的打字系统越复杂,使用起来就越不愉快。这不是一条硬性规定,但我认为这在很大程度上是正确的。与任何正式的系统一样,您经常会发现,表达证明比首先创建实现更为复杂(而且更容易出错)。

理论上 使用它来证明关于代码的任何可判定属性,前提是您编写代码的方式使其能够接受此类证明。Haskell几乎可以肯定是比Java更好的语言(因为Haskell中的类型级编程类似于Prolog,而Scala中的类型级编程更类似于SML)。我不建议您以这种方式使用Scala或Haskell的类型系统(算法正确性的形式证明),但是理论上这个选项是可用的。

总之,我认为你在“现实世界”中没有看到形式系统的原因,是因为形式证明系统已经屈服于实用主义的无情专制。正如我所提到的,在你的正确性证明中有太多的工作要做,这几乎是不值得的。很久以前,业界就认为创建特别的测试比进行任何形式的分析性推理过程都要容易。

为了证明一个完整的程序是有效的,是的,你正在超越普通语言的界限,数学和编程在这里相遇,握手,然后继续用希腊语符号谈论程序员如何不能处理希腊语符号。不管怎么说,这是最重要的。

你在问一个我们很多人多年来都问过的问题。我不知道我有一个很好的答案,但这里有一些:

• 有一些理解良好的语言可以在今天被证明是可用的;Lisp via ACL2就是其中之一,Scheme当然也有一个理解良好的形式定义。

• 回溯到20多年前,有一种使用正式语言的手工证明的方法很短暂,后来被严格地翻译成编译语言。例如IBM的软件clearnoom、ACL、Gypsy和Rose out Computational Logic、John McHugh和我在可信的C编译方面的工作,以及我自己在C系统编程方面的手证工作。这些都引起了一些注意,但没有一个付诸实践。

我想,一个有趣的问题是,什么才是使正式方法付诸实践的充分条件?我想听一些建议。

你可以调查 纯函数语言 就像Haskell,当您的需求之一是 可证明性

This 如果你对函数式编程语言和纯函数式编程语言感兴趣的话,这是一本有趣的读物。

商业世界需要工作软件,快。

“可证明”语言只是不适合于编写/读取大型项目的代码库,而且似乎只适用于小型和独立的用例。

我涉及两种可证明的语言。第一种是Perfect Developer支持的语言,这是一个用于指定sotfware、优化sotfware并生成代码的系统。它已经被用于一些大型系统,包括PD本身,并且在一些大学里教授。我所涉及的第二种可证明语言是MISRA-C的可证明子集,请参见 C/C++ Verification Blog

退房 Omega .

这个 introduction

编辑===== 删除了我关于ML是“可证明的”的错误想法。

在可证明正确的代码中,我对“真实世界”的(有争议的)定义是:

• 自动化
• 它必须支持某种程度的 ,这有助于您编写非常模块化、可重用且易于推理的代码。显然,编写或证明Hello World或各种简单程序并不需要函数式编程,但在某种程度上,函数式编程确实变得非常有用。
• 虽然你不一定非得能用主流编程语言编写代码,但作为一种替代方案,你至少应该能够以可靠的方式将代码机器翻译成用主流编程语言编写的相当有效的代码。

鉴于这些观点,在 this blog post of mine 可能有用——尽管它们几乎都是新的和实验性的,或者对绝大多数行业程序员来说是陌生的。不过,这里有一些非常成熟的工具。

Idris 和 Agda

作为一个很好的现实例子,有一个项目旨在提供一个用Agda编写的经过验证的HTTP REST库,称为Lemmachine: https://github.com/larrytheliquid/Lemmachine