Yes, there are languages designed for writing provably correct software. Some are even used in industry. Spark Ada is probably the most prominent example. I've talked to a few people at Praxis Critical Systems Limited who used it for code running on Boings (for engine monitoring) and it seems quite nice. (Here is a great summary / description of the language.) This language and accompanying proof system uses the second technique described below. It doesn't even support dynamic memory allocation!
My impression and experience is that there are two techniques for writing correct software:
Technique 1: Write the software in a language you're comfortable with (C, C++ or Java for instance). Take a formal specification of such language, and prove your program correct.
If your ambition is to be 100% correct (which is most often a requirement in automobile / aerospace industry) you'd be spending little time programming, and more time proving.
Technique 2: Write the software in a slightly more awkward language (some subset of Ada or tweaked version of OCaml for instance) and write the correctness proof along the way. Here programming and proving goes hand in hand. Programming in Coq even equates them completely! (See the Curry-Howard correspondence)
In these scenarios you'll always end up with a correct program. (A bug will be guaranteed to be rooted in the specification.) You'll be likely to spend more time on programming but on the other hand you're proving it correct along the way.
Note that both approaches hinges on the fact you have a formal specification at hand (how else would you tell what is correct / incorrect behavior), and a formally defined semantics of the language (how else would you be able to tell what the actual behavior of your program is).
Here are a few more examples of formal approaches. If it's "real-world" or not, depends on who you ask :-)
In order to answer this question, you really need to define what you mean by "provable". As Ricky pointed out, any language with a type system is a language with a built-in proof system which runs every time you compile your program. These proof systems are almost always sadly impotent — answering questions like String vs Int and avoiding questions like "is the list sorted?" — but they are proof systems none-the-less.
Unfortunately, the more sophisticated your proof goals, the harder it is to work with a system which can check your proofs. This escalates pretty quickly into undecidability when you consider the sheer size of the class of problems which are undecidable on Turing Machines. Sure, you can theoretically do basic things like proving the correctness of your sorting algorithm, but anything more than that is going to be treading on very thin ice.
Even to prove something simple like the correctness of a sorting algorithm requires a comparatively sophisticated proof system. (note: since we have already established that type systems are a proof system built into the language, I'm going to talk about things in terms of type theory, rather than waving my hands still more vigorously) I'm fairly certain that a full correctness proof on list sorting would require some form of dependent types, otherwise you have no way of referencing relative values at the type level. This immediately starts breaking into realms of type theory which have been shown to be undecidable. So, while you may be able to prove correctness on your list sorting algorithm, the only way to do it would be to use a system which will also allow you to express proofs which it cannot verify. Personally, I find this very disconcerting.
There is also the ease-of-use aspect which I alluded to earlier. The more sophisticated your type system, the less pleasant it is to use. That's not a hard and fast rule, but I think it holds true for the most part. And as with any formal system, you will often find that expressing the proof is more work (and more error prone) than creating the implementation in the first place.
With all that out of the way, it's worth noting that Scala's type system (like Haskell's) is Turing Complete, which means that you can theoretically use it to prove any decidable property about your code, provided that you have written your code in such a way that it is amenable to such proofs. Haskell is almost certainly a better language for this than Java (since type-level programming in Haskell is similar to Prolog, while type-level programming in Scala is more similar to SML). I don't advise that you use Scala's or Haskell's type systems in this way (formal proofs of algorithmic correctness), but the option is theoretically available.
Altogether, I think the reason you haven't seen formal systems in the "real world" stems from the fact that formal proof systems have yielded to the merciless tyranny of pragmatism. As I mentioned, there's so much effort involved in crafting your correctness proofs that it's almost never worthwhile. The industry decided a long time ago that it was easier to create ad hoc tests than it was to go through any sort of analytical formal reasoning process.
回溯 20 多年，使用正式语言的手工校对然后严格翻译成编译语言的做法是短暂的。一些例子包括 IBM 的 Software Cleanroom、ACL、Gypsy 和计算逻辑中的 Rose，John McHugh 和我在 C 的可信编译方面的工作，以及我自己在 C 系统编程的手工验证方面的工作。这些都引起了一些关注，但都没有付诸实践。
我认为一个有趣的问题是将正式方法付诸实践的充分条件是什么？我很想听听一些建议。
You're asking a question a lot of us have asked over the years. I don't know that I have a good answer, but here are some pieces:
There are well-understood languages with the possibility of being proven in use today; Lisp via ACL2 is one, and of course Scheme has a well-understood formal definition as well.
a number of systems have tried to use pure functional languages, or nearly pure ones, like Haskell. There's a fair bit of formal methods work in Haskell.
Going back 20+ years, there was a short-lived thing for using hand-proof of a formal language which was then rigorously translated into a compiled language. Some examples were IBM's Software Cleanroom, ACL, Gypsy, and Rose out of Computational Logic, John McHugh's and my work on trustworthy compilation of C, and my own work on hand-proof for C systems programming. These all got some attention, but none of them made it much into practice.
An interesting question to ask, I think, is what would sufficient conditions be to get formal approaches into practice? I'd love to hear some suggestions.
Typed languages prove the absence of certain categories of fault. The more advanced the type system, the more faults they can prove the absence of.
For proof that a whole program works, yes, you're stepping outside the boundaries of ordinary languages, where mathematics and programming meet each other, shake hands and then proceed to talk using Greek symbols about how programmers can't handle Greek symbols. That's about the Σ of it anyway.
real world uses of such provable languages would be incredibly difficult to write and understand afterwoods. the business world needs working software, fast.
"provable" languages just dont scale for writing/reading a large project's code base and only seem to work in small and isolated use cases.
I'm involved in two provable languages. The first is the language supported by Perfect Developer, a system for specifying sotfware, refining it and generating code. It's been used for some large systems, including PD itself, and it's taught in a number of universities. The second provable language I'm involved with is a provable subset of MISRA-C, see C/C++ Verification Blog for more.
Scala is meant to be "real world", so no effort has been made to make it provable. What you can do in Scala is to produce functional code. Functional code is much easier to test, which is IMHO a good compromise between "real world" and provability.
EDIT ===== Removed my incorrect ideas about ML being "provable".
My (controversial) definition of "real-world" in the context of provably-correct code is:
It must involve some degree of automation, otherwise you're going to spend far too much time proving and dealing with messy little details, and it's going to be totally impractical (except maybe for spacecraft control software and that sort of thing, for which you might actually want to spend megabucks on meticulous checks).
It must support some degree of functional programming, which helps you write code that is very modular, reusable and easier to reason about. Obviously functional programming isn't needed for writing or proving Hello World, or a variety of simple programs, but at a certain point, functional programming does become very useful.
While you don't necessarily have to be able to write your code in a mainstream programming language, as an alternative, you should at least be able to machine-translate your code into reasonably efficient code written in a mainstream programming language, in a reliable way.
The above are relatively more universal requirements. Others, such as the ability to model imperative code, or the ability to prove higher-order functions correct, may be important or essential for some tasks, but not all.
In view of these points, many of the tools listed in this blog post of mine may be useful - although they are nearly all either new and experimental, or unfamiliar to the vast majority of industry programmers. There are some very mature tools covered there though.
As a good real life example, there's a project that aims to provide a verified HTTP REST library written in Agda, called Lemmachine: https://github.com/larrytheliquid/Lemmachine
发布评论
评论（11）
是的，有些语言是为编写可证明正确的软件而设计的。有些甚至用于工业。 Spark Ada 可能是最突出的例子。我和 Praxis Critical Systems Limited 的一些人交谈过，他们使用它来在 Boings 上运行代码（用于引擎监控），它看起来相当不错。 （这里有一个很棒的该语言的摘要/描述.) 该语言和随附的证明系统使用下面描述的第二种技术。它甚至不支持动态内存分配！
我的印象和经验是，编写正确的软件有两种技术：
技术 1：用您熟悉的语言（例如 C、C++ 或 Java）编写软件。采用此类语言的正式规范，并证明您的程序是正确的。
如果您的目标是 100% 正确（这是汽车/航空航天行业最常见的要求），您将花费很少的时间进行编程，而花费更多的时间来证明。
技术 2：用稍微尴尬的语言（例如 Ada 的某些子集或 OCaml 的调整版本）编写软件，并一路编写正确性证明。在这里，编程和证明是齐头并进的。在 Coq 中编程甚至完全等同于它们！ （请参阅Curry-Howard 对应关系）
在这些情况下，您总是会得到正确的程序。 （错误肯定会根植于规范中。）您可能会在编程上花费更多时间，但另一方面，您会一路证明它的正确性。
请注意，这两种方法都取决于您手头有一个正式的规范（否则您如何判断什么是正确/不正确的行为），以及语言的正式定义的语义（您如何才能判断实际行为）你的程序是）。
以下是正式方法的更多示例。如果它是“真实世界”与否，取决于你问的是谁:-)
我只知道一种“可证明正确的”网络应用程序语言：UR. “通过编译器”的 Ur 程序保证不会：
Yes, there are languages designed for writing provably correct software. Some are even used in industry. Spark Ada is probably the most prominent example. I've talked to a few people at Praxis Critical Systems Limited who used it for code running on Boings (for engine monitoring) and it seems quite nice. (Here is a great summary / description of the language.) This language and accompanying proof system uses the second technique described below. It doesn't even support dynamic memory allocation!
My impression and experience is that there are two techniques for writing correct software:
Technique 1: Write the software in a language you're comfortable with (C, C++ or Java for instance). Take a formal specification of such language, and prove your program correct.
If your ambition is to be 100% correct (which is most often a requirement in automobile / aerospace industry) you'd be spending little time programming, and more time proving.
Technique 2: Write the software in a slightly more awkward language (some subset of Ada or tweaked version of OCaml for instance) and write the correctness proof along the way. Here programming and proving goes hand in hand. Programming in Coq even equates them completely! (See the Curry-Howard correspondence)
In these scenarios you'll always end up with a correct program. (A bug will be guaranteed to be rooted in the specification.) You'll be likely to spend more time on programming but on the other hand you're proving it correct along the way.
Note that both approaches hinges on the fact you have a formal specification at hand (how else would you tell what is correct / incorrect behavior), and a formally defined semantics of the language (how else would you be able to tell what the actual behavior of your program is).
Here are a few more examples of formal approaches. If it's "real-world" or not, depends on who you ask :-)
I know of only one "provably correct" web-application language: UR. A Ur-program that "goes through the compiler" is guaranteed not to:
为了回答这个问题，您确实需要定义“可证明”的含义。正如 Ricky 指出的那样，任何具有类型系统的语言都是具有内置证明系统的语言，该系统在每次编译程序时都会运行。遗憾的是，这些证明系统几乎总是无能为力——回答诸如
String与Int之类的问题，并避免诸如“列表是否已排序？”之类的问题。 ——但它们仍然是证明系统。不幸的是，您的证明目标越复杂，使用可以检查您的证明的系统就越困难。当您考虑图灵机上不可判定的问题类别的庞大规模时，这种情况很快就会升级为不可判定性。当然，理论上你可以做一些基本的事情，比如证明排序算法的正确性，但除此之外的任何事情都将如履薄冰。
即使要证明一些简单的事情，比如排序算法的正确性，也需要相对复杂的证明系统。 （注意：由于我们已经确定类型系统是语言中内置的证明系统，因此我将根据类型理论来谈论事物，而不是更加有力地挥舞我的手）我相当确定列表排序的完整正确性证明需要某种形式的依赖类型，否则您无法在类型级别引用相对值。这立即开始突破类型理论的领域，这些领域已被证明是不可判定的。因此，虽然您可能能够证明列表排序算法的正确性，但唯一的方法是使用一个系统，该系统也允许您表达它无法验证的证明。就我个人而言，我觉得这非常令人不安。
还有我之前提到的易用性方面。你的类型系统越复杂，使用起来就越不舒服。这不是一个硬性规定，但我认为它在大多数情况下都是正确的。与任何正式系统一样，您通常会发现表达证明比首先创建实现需要更多工作（并且更容易出错）。
考虑到所有这些，值得注意的是 Scala 的类型系统（如 Haskell 的类型系统）是图灵完备的，这意味着您可以理论上使用它来证明关于您的代码的任何可判定属性，前提是您已经以适合此类证明的方式编写了您的代码。几乎可以肯定，Haskell 是一种比 Java 更好的语言（因为 Haskell 中的类型级编程类似于 Prolog，而 Scala 中的类型级编程更类似于 SML）。我不建议您以这种方式使用 Scala 或 Haskell 的类型系统（算法正确性的形式证明），但该选项理论上是可用的。
总而言之，我认为你在“现实世界”中没有看到正式系统的原因源于这样一个事实：正式证明系统已经屈服于实用主义的无情暴政。正如我所提到的，制作正确性证明需要付出如此多的努力，而这几乎是不值得的。业界很久以前就决定，创建临时测试比经历任何类型的分析形式推理过程更容易。
In order to answer this question, you really need to define what you mean by "provable". As Ricky pointed out, any language with a type system is a language with a built-in proof system which runs every time you compile your program. These proof systems are almost always sadly impotent — answering questions like
StringvsIntand avoiding questions like "is the list sorted?" — but they are proof systems none-the-less.Unfortunately, the more sophisticated your proof goals, the harder it is to work with a system which can check your proofs. This escalates pretty quickly into undecidability when you consider the sheer size of the class of problems which are undecidable on Turing Machines. Sure, you can theoretically do basic things like proving the correctness of your sorting algorithm, but anything more than that is going to be treading on very thin ice.
Even to prove something simple like the correctness of a sorting algorithm requires a comparatively sophisticated proof system. (note: since we have already established that type systems are a proof system built into the language, I'm going to talk about things in terms of type theory, rather than waving my hands still more vigorously) I'm fairly certain that a full correctness proof on list sorting would require some form of dependent types, otherwise you have no way of referencing relative values at the type level. This immediately starts breaking into realms of type theory which have been shown to be undecidable. So, while you may be able to prove correctness on your list sorting algorithm, the only way to do it would be to use a system which will also allow you to express proofs which it cannot verify. Personally, I find this very disconcerting.
There is also the ease-of-use aspect which I alluded to earlier. The more sophisticated your type system, the less pleasant it is to use. That's not a hard and fast rule, but I think it holds true for the most part. And as with any formal system, you will often find that expressing the proof is more work (and more error prone) than creating the implementation in the first place.
With all that out of the way, it's worth noting that Scala's type system (like Haskell's) is Turing Complete, which means that you can theoretically use it to prove any decidable property about your code, provided that you have written your code in such a way that it is amenable to such proofs. Haskell is almost certainly a better language for this than Java (since type-level programming in Haskell is similar to Prolog, while type-level programming in Scala is more similar to SML). I don't advise that you use Scala's or Haskell's type systems in this way (formal proofs of algorithmic correctness), but the option is theoretically available.
Altogether, I think the reason you haven't seen formal systems in the "real world" stems from the fact that formal proof systems have yielded to the merciless tyranny of pragmatism. As I mentioned, there's so much effort involved in crafting your correctness proofs that it's almost never worthwhile. The industry decided a long time ago that it was easier to create ad hoc tests than it was to go through any sort of analytical formal reasoning process.
你问的是我们很多人多年来都问过的问题。我不知道我有一个很好的答案，但这里有一些：
有一些易于理解的语言，有可能在今天被证明可以使用； Lisp via ACL2 就是其中之一，当然，Scheme 也有一个易于理解的形式定义。
许多系统尝试使用纯函数式语言，或接近纯的语言，例如 Haskell。 Haskell 中有相当多的形式化方法。
回溯 20 多年，使用正式语言的手工校对然后严格翻译成编译语言的做法是短暂的。一些例子包括 IBM 的 Software Cleanroom、ACL、Gypsy 和计算逻辑中的 Rose，John McHugh 和我在 C 的可信编译方面的工作，以及我自己在 C 系统编程的手工验证方面的工作。这些都引起了一些关注，但都没有付诸实践。
我认为一个有趣的问题是将正式方法付诸实践的充分条件是什么？我很想听听一些建议。
You're asking a question a lot of us have asked over the years. I don't know that I have a good answer, but here are some pieces:
There are well-understood languages with the possibility of being proven in use today; Lisp via ACL2 is one, and of course Scheme has a well-understood formal definition as well.
a number of systems have tried to use pure functional languages, or nearly pure ones, like Haskell. There's a fair bit of formal methods work in Haskell.
Going back 20+ years, there was a short-lived thing for using hand-proof of a formal language which was then rigorously translated into a compiled language. Some examples were IBM's Software Cleanroom, ACL, Gypsy, and Rose out of Computational Logic, John McHugh's and my work on trustworthy compilation of C, and my own work on hand-proof for C systems programming. These all got some attention, but none of them made it much into practice.
An interesting question to ask, I think, is what would sufficient conditions be to get formal approaches into practice? I'd love to hear some suggestions.
类型化语言证明不存在某些类别的错误。类型系统越先进，它们可以证明不存在的错误就越多。
为了证明整个程序有效，是的，您正在走出普通语言的界限，数学和编程在这里相遇，握手，然后继续使用希腊符号谈论程序员如何无法处理希腊符号。无论如何，这大约是它的 Σ 。
Typed languages prove the absence of certain categories of fault. The more advanced the type system, the more faults they can prove the absence of.
For proof that a whole program works, yes, you're stepping outside the boundaries of ordinary languages, where mathematics and programming meet each other, shake hands and then proceed to talk using Greek symbols about how programmers can't handle Greek symbols. That's about the Σ of it anyway.
在现实世界中使用这种可证明的语言将很难编写和理解。
商业世界需要快速运行的软件。
“可证明”语言无法扩展用于编写/读取大型项目的代码库，并且似乎只能在小型且孤立的用例中工作。
real world uses of such provable languages would be incredibly difficult to write and understand afterwoods.
the business world needs working software, fast.
"provable" languages just dont scale for writing/reading a large project's code base and only seem to work in small and isolated use cases.
我涉及两种可证明的语言。第一个是 Perfect Developer 支持的语言，这是一个用于指定软件、改进软件并生成代码的系统。它已被用于一些大型系统，包括 PD 本身，并且在许多大学中都有教授。我涉及的第二种可证明语言是 MISRA-C 的可证明子集，请参阅 C/C++ 验证博客了解更多的。
I'm involved in two provable languages. The first is the language supported by Perfect Developer, a system for specifying sotfware, refining it and generating code. It's been used for some large systems, including PD itself, and it's taught in a number of universities. The second provable language I'm involved with is a provable subset of MISRA-C, see C/C++ Verification Blog for more.
请查看Omega。
这个简介包含 AVL 树的相对轻松的实现，并包含正确性证明。
Check out Omega.
This introduction contains a relatively painless implementation of AVL trees with included correctness proof.
您可以研究像 Haskell 这样的纯函数式语言，当您的需求之一是可证明性时，可以使用这些语言。
如果您对函数式编程语言和纯函数式编程语言感兴趣，这是一本有趣的读物。
You can investigate purely functional languages like Haskell, which are used when one of your requirements is provability.
This is a fun read if you're interested about functional programming languages and pure functional programming languages.
Scala 旨在成为“现实世界”，因此没有做出任何努力来证明它。在 Scala 中你可以做的是生成函数代码。功能代码更容易测试，恕我直言，这是“现实世界”和可证明性之间的一个很好的折衷。
编辑=====
删除了我关于 ML 是“可证明的”的错误想法。
Scala is meant to be "real world", so no effort has been made to make it provable. What you can do in Scala is to produce functional code. Functional code is much easier to test, which is IMHO a good compromise between "real world" and provability.
EDIT =====
Removed my incorrect ideas about ML being "provable".
在可证明正确的代码的背景下，我对“现实世界”的（有争议的）定义是：
以上是相对比较普遍的要求。其他的，例如对命令式代码进行建模的能力，或者证明高阶函数正确的能力，对于某些任务可能很重要或必不可少，但不是全部。
鉴于这些点，此博客中列出的许多工具我的帖子可能有用 - 尽管它们几乎都是新的和实验性的，或者对绝大多数行业程序员来说是不熟悉的。不过，其中涵盖了一些非常成熟的工具。
My (controversial) definition of "real-world" in the context of provably-correct code is:
The above are relatively more universal requirements. Others, such as the ability to model imperative code, or the ability to prove higher-order functions correct, may be important or essential for some tasks, but not all.
In view of these points, many of the tools listed in this blog post of mine may be useful - although they are nearly all either new and experimental, or unfamiliar to the vast majority of industry programmers. There are some very mature tools covered there though.
Idris 和 Agda？现实世界够了吗？
作为一个很好的现实例子，有一个项目旨在提供一个用 Agda 编写的经过验证的 HTTP REST 库，称为 Lemmachine： https ://github.com/larrytheliquid/Lemmachine
How about Idris and Agda? Real world enough?
As a good real life example, there's a project that aims to provide a verified HTTP REST library written in Agda, called Lemmachine: https://github.com/larrytheliquid/Lemmachine