我在大学里被教过关于正规系统的知识，但是令我失望的是，它们似乎并没有被真正的单词使用。
我喜欢这样的想法：能够知道某些代码（对象，函数，任何东西）起作用，而不是通过测试，而是通过 证明 。
我确定我们都熟悉物理工程和软件工程之间不存在的相似之处（钢铁的行为可预测，软件可以做任何事情- 谁知道！），我很想知道是否有任何语言可以可以用真实的词来使用（是否要求太多Web框架？）
我听说过有关诸如scala之类的功能语言的可测试性的有趣事情。
作为软件 工程师 ，我们有哪些选择？
是的，有些语言旨在编写可证明正确的软件。有些甚至用于工业。Spark Ada可能是最突出的例子。我已经与Praxis Critical Systems Limited的一些人进行了交谈，他们将其用于在Boings上运行的代码（用于引擎监视），这看起来非常不错。（以下是该语言的精彩摘要/说明。）此语言及其随附的证明系统使用下面描述的第二种技术。它甚至不支持动态内存分配！
我的印象和经验是，有两种技术可以编写正确的软件：
如果您的目标是100％正确（这在汽车/航空航天业通常是必需的），那么您将花费很少的时间进行编程，而花费更多的时间进行证明。
在这些情况下，您总是会得到正确的程序。（一定会保证错误会根植于规范中。）您可能会花更多的时间在编程上，但另一方面，您会在此过程中证明它是正确的。
请注意，这两种方法都取决于您手头有一个正式的规范（您将如何分辨正确/不正确的行为）以及该语言的形式化语义（您将如何分辨实际的行为）您的程序是）。
这是正式方法的更多示例。是否是“真实世界”，取决于您问的人:-)
我只知道一种“证明正确的” Web应用程序语言 ：UR。确保“经过编译器”的Ur程序不会：
