有没有任何可certificate的现实世界的语言？ （Scala呢？）
我在大学里接受过正规系统的教育，但是我感到失望，他们似乎并没有被用在真正的词汇中。
我喜欢能够知道一些代码（对象，函数，任何）的工作原理，而不是通过testing，而是通过certificate 。
我相信我们都熟悉物理工程和软件工程之间不存在的相似之处（钢铁的performance可以预见，软件可以做任何事 – 谁知道！），我很想知道是否有任何语言可以用在真正的词（是要求一个Web框架太多问）？
我听说过有趣的function语言如scala的可testing性。
作为软件工程师 ，我们有什么select？
是的，有些语言是为了编写正确的软件而devise的。 有些甚至用于工业。 Spark Ada可能是最突出的例子。 我曾经和Praxis Critical Systems Limited的几个人谈过，他们用Boings上的代码（用于引擎监视），看起来相当不错。 （以下是对该语言的一个很好的总结/描述 。）这种语言和伴随certificate系统使用下面描述的第二种技术。 它甚至不支持dynamic内存分配！
我的印象和经验是有两个技巧来编写正确的软件：
-
技巧1：用您熟悉的语言（例如C，C ++或Java）编写软件。 采取这种语言的正式说明，并certificate你的程序是正确的。
如果你的抱负是100％正确的（这在汽车/航空航天工业中通常是必需的），那么你将花费很less的时间进行编程，而且时间更多。
-
技巧2：用稍微笨拙的语言（例如Ada的一些子集或OCaml的调整版本）编写软件，并且一路书写正确性certificate。 这里的编程和validation是齐头并进的。 编程在Coq甚至完全等同于他们！ （见咖喱霍华德对应 ）
在这些情况下，你总是会得到一个正确的程序。 （一个错误将被保证在规范中生根。）你可能会花更多的时间在编程上，但是另一方面，你在这个过程中certificate了它是正确的。
请注意，这两种方法取决于你有一个正式的规范（你怎么会告诉什么是正确/不正确的行为），还有一个正式定义的语言的语义（你还能怎么知道实际的行为你的程序是）。
以下是一些正式方法的例子。 如果是“真实世界”，取决于你问谁:-)
- Coq定理certificate书： 用Coq编程 （技术2）
- ESC / Java （技术1，虽然声音也不完整）
- 规范＃ （技术1，既不健全也不完整）
- 为什么/ Krakatoa （技术2，基于Java）
我只知道一个“certificate正确”的networking应用语言 ： UR 。 “通过编译器”的Ur程序保证不会：
- 受到任何types的代码注入攻击
- 返回无效的HTML
- 包含死亡的应用程序内链接
- HTML表单与处理程序期望的字段之间不匹配
- 包括对远程Web服务器提供的“AJAX”风格服务做出错误假设的客户端代码
- 尝试无效的SQL查询
- 与SQL数据库或浏览器和Web服务器之间的通信使用不正确的封送处理或解组处理
为了回答这个问题，你真的需要定义“可certificate”的含义。 正如Ricky所指出的那样，任何具有types系统的语言都是一种内置certificate系统的语言，每次编译程序时都会运行它。 这些certificate系统几乎总是令人伤心 – 回答诸如String和Int问题，并避免像“列表sorting”这样的问题。 – 但他们是certificate系统无所谓。
不幸的是，你的certificate目标越复杂，使用一个可以检查certificate的系统就越难。 当你考虑图灵机上不可判定的这类问题时，这个问题很快会升级成为不可判定的。 当然，理论上你可以做一些基本的事情，例如certificate你的sortingalgorithm的正确性，但是除此之外，任何事情都将在非常薄弱的环境中进行。
即使为了certificate简单的分类algorithm的正确性，也需要相对复杂的certificate系统。 （注意：由于我们已经确定了types系统是一种内置于语言中的certificate系统，所以我将用types论的方式来谈论事情，而不是更有力地挥动我的手）我确信完整的列表sorting正确性certificate需要某种forms的依赖types，否则你无法在types级别引用相对值。 这立即开始打破已被certificate是不可判定的types理论领域。 所以，虽然你可能能够certificate你的列表sortingalgorithm的正确性，唯一的方法是使用一个系统，它也将允许你expressioncertificate，它不能validation。 我个人觉得这很令人不安。
还有我早些时候提到的易用性方面。 你的types系统越复杂，使用起来就越不愉快。 这不是一个硬性规定，但我认为大部分情况是正确的。 和任何正式的系统一样，你经常会发现，expression证据比起首先创build实现更有效（更容易出错）。
除此之外，值得注意的是，Scala的types系统（像Haskell的）是Turing Complete，这意味着你可以理论上使用它来certificate你的代码的任何可判定的属性，只要你已经写了这样的代码这样的证据是可以接受的。 Haskell几乎肯定是比Java更好的语言（因为Haskell中的types级编程类似于Prolog，而Scala中的types级编程更类似于SML）。 我不build议你以这种方式使用Scala或Haskelltypes的系统（algorithm正确性的formscertificate），但是这个选项在理论上是可用的。
总而言之，我认为你在“现实世界”中没有看到正式系统的原因是由于formscertificate体系已经屈服于无情的实用主义暴政。 正如我所提到的，在制定正确性certificate中涉及到很多努力，这几乎是不值得的。 业内人士很久以前就决定，创build临时testing比通过任何forms的分析forms推理过程更容易。
键入的语言certificate缺less某些类别的错误。 types系统越先进，他们可以certificate缺less更多的错误。
为了certificate整个程序的工作，是的，你正在超越普通语言的界限，在那里math和程序devise相互交stream，握手，然后用希腊符号谈谈程序员如何处理希腊符号。 无论如何，这是关于它的Σ。
你问了我们很多年来问过的一个问题。 我不知道我有一个好的答案，但这里有一些片段：
-
有很好理解的语言可能被certificate在今天使用; Lisp通过ACL2是一个，当然Scheme也有一个很好理解的正式定义。
-
许多系统试图使用纯粹的函数式语言，或者像Haskell那样接近纯粹的函数式语言。 Haskell中有一些正式的方法可以工作。
-
回顾20多年来，用一种forms语言的手工certificate是一个短暂的事情，然后严格地翻译成一种编译语言。 一些例子是IBM的软件洁净室，ACL，吉普赛和玫瑰计算逻辑，约翰McHugh和我的工作值得信赖的编译C和我自己的C系统编程的手工certificate工作。 这些都受到了一些关注，但没有一个在实践中付出了很多努力。
我想问一个有趣的问题，就是有足够的条件去实践正式的方法吗？ 我很想听听一些build议。
您可以调查像Haskell这样的纯函数式语言 ，当您的要求之一是可certificate性时使用 。
如果您对函数式编程语言和纯函数式编程语言感兴趣， 这是一个有趣的阅读。
真正的世界使用这种可certificate的语言将是难以置信的难以写和理解后森林。 商业世界需要工作软件，快速。
“可certificate的”语言只是不能用于写/读大型项目的代码库的规模，而只能在小而孤立的用例中工作。
我参与了两个可certificate的语言。 第一种是Perfect Developer支持的语言，它是一个指定软件，提炼和生成代码的系统。 它已被用于一些大型系统，包括PD本身，并在一些大学教授。 我参与的第二个可certificate的语言是MISRA-C的一个可certificate的子集，更多地参见C / C ++validation博客 。
斯卡拉是为了“真实世界”，所以没有努力使其可certificate。 你可以在Scala中做什么是产生function代码。 function代码更容易testing，这是“真实世界”和可证性之间的一个很好的妥协。
编辑=====删除我关于ML“可certificate”的不正确的想法。
看看欧米茄 。
这个介绍包含了AVL树的一个相对简单的实现，包含了正确性certificate。
在可certificate正确的代码中，我的（有争议的）“现实世界”的定义是：
- 它必须涉及到一定程度的自动化 ，否则你将花费太多的时间来certificate和处理凌乱的小细节，这将是完全不切实际的（除了可能的飞船控制软件和那种事情，为此实际上可能会花费巨大的精力检查）。
- 它必须支持一定程度的函数式编程 ，这可以帮助您编写非常模块化，可重用且易于推理的代码。 很显然，编写或者validationHello World或者各种简单的程序都不需要函数式编程，但是在某个时候，函数式编程确实变得非常有用。
- 虽然您不一定必须能够使用主stream编程语言编写代码，但作为替代，您至less应该能够将代码机器翻译成用主stream编程语言编写的相当高效的代码，并且可靠办法。
以上是比较普遍的要求。 其他的，如模拟命令式代码的能力，或certificate高阶函数正确的能力，对于某些任务可能是重要的或必不可less的，但并非全部。
鉴于这些观点， 我的这篇博文中列出的许多工具可能是有用的，尽pipe它们几乎都是新的和实验性的，或者是绝大多数行业程序员都不熟悉的。 那里有一些非常成熟的工具。
伊德里斯和阿格达呢？ 真实世界够了吗？
作为一个很好的现实生活的例子，有一个项目旨在提供一个经过validation的用Agda编写的HTTP REST库，名为Lemmachine： https ： //github.com/larrytheliquid/Lemmachine
