我在大学里被教导过正式系统，但令我失望的是，它们似乎没有在真正的单词中使用。
我喜欢能够知道某些代码（对象，函数，等等）工作的想法，不是通过测试，而是通过证明。
我相信我们都熟悉物理工程和软件工程之间不存在的相似之处（钢铁行为是可预测的，软件可以做任何事情 - 谁知道呢！），我很想知道是否有任何语言可以在真实单词中使用（要求Web框架太多了吗？
我听说过关于 scala 等函数式语言的可测试性的有趣事情。
作为软件工程师，我们有哪些选择？
是的，有一些语言是为编写可证明正确的软件而设计的。有些甚至用于工业。Spark Ada可能是最突出的例子。我和Praxis Critical Systems Limited的几个人谈过，他们用它来编写在Boings上运行的代码（用于引擎监控），这似乎很不错。（这是该语言的一个很好的摘要/描述。这种语言和随附的证明系统使用下面描述的第二种技术。它甚至不支持动态内存分配！
我的印象和经验是，有两种技术可以编写正确的软件：
技巧1：用你熟悉的语言（例如C，C++或Java）编写软件。采用这种语言的正式规范，并证明你的程序是正确的。
如果你的雄心壮志是100%正确（这通常是汽车/航空航天工业的要求），那么你将花费很少的时间编程，而花更多的时间进行验证。
技术2：用稍微笨拙的语言编写软件（例如Ada的一些子集或OCaml的调整版本），并在此过程中编写正确性证明。在这里，编程和验证是齐头并进的。在Coq中编程甚至将它们完全等同于它们！（参见库里-霍华德通信)
在这些情况下，您始终会得到一个正确的程序。（一个错误将保证植根于规范中。你可能会花更多的时间在编程上，但另一方面，你一路上证明它是正确的。
请注意，这两种方法都取决于你手头有一个正式的规范（否则你如何判断什么是正确的/不正确的行为），以及一个正式定义的语言语义（否则你怎么能知道你的程序的实际行为是什么）。
以下是一些正式方法的更多示例。如果它是“现实世界”与否，取决于你问谁：-）
我只知道一种“可证明正确”的Web应用程序语言：UR。“通过编译器”的程序保证不会：
为了回答这个问题，你真的需要定义你所说的“可证明”是什么意思。正如Ricky所指出的，任何具有类型系统的语言都是具有内置证明系统的语言，每次编译程序时都会运行。可悲的是，这些证明系统几乎总是无能为力的——回答像vs这样的问题，避免像“列表是否排序？”这样的问题——但它们是证明系统。StringInt
不幸的是，你的证明目标越复杂，就越难使用一个可以检查你的证明的系统。当你考虑到图灵机上无法决定的问题的绝对规模时，这很快就会升级为不可决定性。当然，从理论上讲，你可以做一些基本的事情，比如证明你的排序算法的正确性，但除此之外的任何事情都将在非常薄的冰上踩踏。
即使要证明像排序算法的正确性这样简单的东西，也需要一个相对复杂的证明系统。（注意：既然我们已经确定类型系统是内置于语言中的证明系统，我将从类型论的角度来谈谈事情，而不是更用力地挥手）我很确定列表排序的完全正确性证明需要某种形式的依赖类型，否则您无法在类型级别引用相对值。这立即开始闯入类型论的领域，这些领域已被证明是不可决定的。因此，虽然您可能能够在列表排序算法上证明正确性，但唯一的方法是使用一个系统，该系统还允许您表达无法验证的证明。就个人而言，我觉得这非常令人不安。
还有我之前提到的易用性方面。您的类型系统越复杂，使用起来就越不愉快。这不是一个硬性规定，但我认为它在大多数情况下都适用。与任何正式系统一样，您经常会发现，与首先创建实现相比，表达证明更多的工作（并且更容易出错）。
考虑到所有这些，值得注意的是，Scala的类型系统（如Haskell的类型系统）是图灵完备的，这意味着理论上你可以用它来证明代码的任何可判定属性，前提是你已经以一种适合这种证明的方式编写了你的代码。Haskell几乎肯定是比Java更好的语言（因为Haskell中的类型级编程类似于Prolog，而Scala中的类型级编程更类似于SML）。我不建议你以这种方式使用Scala或Haskell的类型系统（算法正确性的形式证明），但这个选项在理论上是可用的。
总而言之，我认为你没有在“现实世界”中看到正式系统的原因源于这样一个事实，即正式的证明系统已经屈服于实用主义的无情暴政。正如我所提到的，制作正确性证明涉及如此多的努力，以至于它几乎从来都不值得。业界很久以前就决定，创建临时测试比通过任何类型的分析形式推理过程更容易。
