I have always associated Dijkstra's masterpiece with a model of programming in which center stage is occupied by loops and arrays. If you're sticking close to Dijkstra (e.g., computing weakest preconditions) I think you'll find functional languages are not a great fit. Of the popular languages that provide good support for imperative programming with loops and arrays, perhaps Python carries the least additional baggage.
This is not to say that functional languages are unsuited to formal methods---they are very well suited---but the style is quite different from Dijkstra. The preferred methods emphasize calculational proofs; see Richard Bird's paper on solving Sudoku (which is heavy going) or the textbook by Richard Bird and Phil Wadler.
For concurrency it depends a lot on what model of concurrency (and what formal methods) you believe in. John Reppy's Concurrent ML is a beautiful message-passing model. Erlang also has a nice clean restrictive model. On the other hand, programming with locks and critical sections is so difficult, there may be more benefit to formal methods in that situation.
Two other passing remarks that may be of interest for your background research:
The only programmer I ever met who applied Dijkstra's methods in practice to real systems was Greg Nelson, who was working in Modula-3. (Greg and Mark Manasse wrote the Trestle window system together.) Modula-3 was a very nice language that Digital allowed to die through fecklessness and incompetence. Greg had a nice TOPLAS paper on an extension to Dijkstra's calculus.
Gerard Holzmann's modeling language SPIN is based directly on Dijkstra's language of guarded commands, and it also supports concurrency. Its purpose is model checking, not programming, and there are a few idiosyncracies, but there is a strong connection with formal methods, and it's really great to be able to model check your assertions. Anyone interested in formal methods will want to check it out.
(Edit: Here's a link to the Greg Nelson paper, or one of them. — CRM)
On the one hand, you are trying to demonstrate methods to what are presumed to be intermediate programmers. If you select a single language and bless it as your books language, you will possibly alienate potential readers that don't happen to prefer that language for one reason or another. Since you're demonstrating methods, You have the luxury of using snippets in languages that happen to illustrate your point concisely. For example, the only language available for demonstrating RIIA is probably C++, but this same language is pretty poor for showing how to perform source analysis. Scheme is ideal for source analysis, but doesn't give you very many options for exploring the benefits (and weaknesses) of strong typing. Use many languages.
On the other hand, since you're mainly up to methods of programming, I'm not totally sure you need any real language at all. A well defined notation is just as good, and forces your readers to focus on the point you're making rather than the superficial details of one language or another.
C# 是一种非常容易学习的语言，它拥有快速深入了解并发等主题所需的所有基础知识。 它具有更多的适用性，因为您也可以针对 OO 和 Web 概念。 它也相当受欢迎，你会让公司为员工的书籍付费，这总是有利于销售（“Be a Kick Ass C# Programmer”在费用报销表上比“Modern Lisp Concurrency”走得更远）。
I grew up on Lisp and Scheme and love them both. I think they are great languages to learn from scratch on. But, I'm not sure someone with some programming experience would take to those languages. You're not going to get a lot of hits on Amazon for your book with Scheme in the title. :)
C# is a very easy language to learn and it's got all the basics you would need to dive into topics like concurrency pretty quickly. It has more applicability because you can target OO and web concepts as well. It's also fairly popular and you would get companies paying for their employees books which is always good for sales ("Be a Kick Ass C# Programmer" goes much further on an expense reimbursement sheet than "Concurrency in Modern Lisp").
F# is an interesting language. It's got the functional beauty of a Lisp or Scheme (well not quite, but almost) and it gives you some ability to dive into OOP topics as well as hook into the .NET Framework for UI stuff if you want to spice things up. But, right now, it's obscure.
I can't speak to Ruby, so personally, I would bite the bullet and go with C#.
Honestly, I can't recommend Ruby for this. When I program day-to-day in my commercial world, I like it quite a lot, certainly much more than C or Java. But the semantics of it are so ill-defined that I don't trust it half as much as C where, though I may spend several hours arguing over a statement and consulting that much thicker white book that replaced K&R, I come out in the end fairly convinced that if I've got a conforming compiler (yes, I know, I'm a dreamer, but work with me here) I know what's coming out the other side.
Ruby is wonderful in many ways, but as far as anything formal goes, the twain will never meet.
I'd tend to vote for Haskell myself, because every time I turn around I'm amazed at how much sense everything makes in that language definition. (Though admittedly after only a year or so at it, I'm sure I've not explored half the corners of even Haskell 98.)
And I understand, too, the Dikjstra vs. functional thing; going back and reading his papers he's very much in an imperative world; I am not qualified to say whether he really went the wrong way there. Perhaps I'm just overwhelmed by how good his writing is, as much as his thought. But it did seem to please him, so what about using Algol 60?
That's a nice idea. I think Scheme is a good option as it allows one to put into practice(in the form of libraries) different abstractions with a bare minimum essentials. It is also easy to translate from scheme to a verification system like PVS (http://pvs.csl.sri.com/)
就我个人而言，我会使用 Common Lisp，因为我对此很熟悉，而且它是实现任何概念的绝佳语言。 其他选项可能是 Erlang、Haskell、Ruby 或 Python，甚至可能是某种 ML 方言。 我对C家族（包括C#和Java）有偏见，他们似乎停留在较低层次的概念思考上。
I think that you should yourself have quite some experience in the language you use for your book, or someone proficient to review your code.
Personally, I'd use Common Lisp, since I am familiar with that, and it's a great language to implement any concept. Other options might be Erlang, Haskell, Ruby, or Python, perhaps even some ML dialect. I am biased against the C family (including C# and Java), they seem stuck to a lower level of thinking about concepts.
There are quite a few universities using Perfect Developer for teaching formal methods (disclaimer: I am connected with this product). It is built around a language for expressing specifications, data refinement and algorithms. It has an automatic theorem prover for verification, and a code generator that can produce C++, C# and Java. The design of PD was very much inspired by "A Discipline of Programming", however we found the notation rather impractical for large systems, so the notation has diverged somewhat from Dijktra's.
发布评论
评论（7）
Charlie，
我一直将 Dijkstra 的杰作与循环和数组占据中心舞台的编程模型联系在一起。 如果您坚持使用 Dijkstra（例如，计算最弱的先决条件），我认为您会发现函数式语言不太适合。 在为循环和数组的命令式编程提供良好支持的流行语言中，Python 的附加负担可能最少。
这并不是说函数式语言不适合形式化方法——它们非常适合——但其风格与 Dijkstra 有很大不同。 首选方法强调计算证明； 请参阅理查德·伯德（Richard Bird）关于解决数独（难度很大）的论文或理查德·伯德（Richard Bird）和菲尔·瓦德勒（Phil Wadler）的教科书。
对于并发性，这在很大程度上取决于您相信哪种并发模型（以及哪种形式方法）。John Reppy 的并发 ML 是一个漂亮的消息传递模型。 Erlang 还有一个很好的干净的限制模型。 另一方面，使用锁和临界区进行编程非常困难，在这种情况下，形式化方法可能会有更多好处。
另外两句话可能对您的背景研究感兴趣：
我见过的唯一一位将 Dijkstra 方法实际应用到真实系统的程序员是 Greg Nelson，他在 Modula-3 工作。 （Greg 和 Mark Manasse 一起编写了 Trestle 窗户系统。）
Modula-3 是一种非常好的语言，但 Digital 却因不负责任和无能而消亡。 Greg 有一篇关于 Dijkstra 微积分扩展的很好的 TOPLAS 论文。
Gerard Holzmann 的建模语言 SPIN 直接基于 Dijkstra 的受保护命令语言，并且它还支持并发。 它的目的是模型检查，而不是编程，并且有一些特质，但与形式方法有很强的联系，能够对你的断言进行模型检查真的很棒。 任何对正式方法感兴趣的人都会想检查一下。
（编辑：这是Greg Nelson 纸质材料，或其中之一——CRM）。
Charlie,
I have always associated Dijkstra's masterpiece with a model of programming in which center stage is occupied by loops and arrays. If you're sticking close to Dijkstra (e.g., computing weakest preconditions) I think you'll find functional languages are not a great fit. Of the popular languages that provide good support for imperative programming with loops and arrays, perhaps Python carries the least additional baggage.
This is not to say that functional languages are unsuited to formal methods---they are very well suited---but the style is quite different from Dijkstra. The preferred methods emphasize calculational proofs; see Richard Bird's paper on solving Sudoku (which is heavy going) or the textbook by Richard Bird and Phil Wadler.
For concurrency it depends a lot on what model of concurrency (and what formal methods) you believe in. John Reppy's Concurrent ML is a beautiful message-passing model. Erlang also has a nice clean restrictive model. On the other hand, programming with locks and critical sections is so difficult, there may be more benefit to formal methods in that situation.
Two other passing remarks that may be of interest for your background research:
The only programmer I ever met who applied Dijkstra's methods in practice to real systems was Greg Nelson, who was working in Modula-3. (Greg and Mark Manasse wrote the Trestle window system together.)
Modula-3 was a very nice language that Digital allowed to die through fecklessness and incompetence. Greg had a nice TOPLAS paper on an extension to Dijkstra's calculus.
Gerard Holzmann's modeling language SPIN is based directly on Dijkstra's language of guarded commands, and it also supports concurrency. Its purpose is model checking, not programming, and there are a few idiosyncracies, but there is a strong connection with formal methods, and it's really great to be able to model check your assertions. Anyone interested in formal methods will want to check it out.
(Edit: Here's a link to the Greg Nelson paper, or one of them. — CRM)
忽略明显的你最喜欢的 编程 语言答案，我可以看到两个有用的答案：
一方面，你试图演示什么方法被认为是中级程序员。 如果您选择一种语言并祝福它作为您的书籍语言，您可能会疏远由于某种原因不喜欢该语言的潜在读者。 由于您正在演示方法，因此您可以使用语言中的片段来简洁地说明您的观点。 例如，可用于演示 RIIA 的唯一语言可能是 C++，但这种语言对于演示如何执行源代码分析来说相当糟糕。 方案非常适合源代码分析，但没有为您提供太多选项来探索强类型的优点（和缺点）。 使用多种语言。
另一方面，由于您主要了解编程方法，因此我不完全确定您是否需要任何真正的语言。 定义良好的符号也同样好，它可以迫使读者将注意力集中在您所表达的观点上，而不是一种语言或另一种语言的表面细节上。
Ignoring the obvious what's your favorite programming language answers, I can see two useful answers:
On the one hand, you are trying to demonstrate methods to what are presumed to be intermediate programmers. If you select a single language and bless it as your books language, you will possibly alienate potential readers that don't happen to prefer that language for one reason or another. Since you're demonstrating methods, You have the luxury of using snippets in languages that happen to illustrate your point concisely. For example, the only language available for demonstrating RIIA is probably C++, but this same language is pretty poor for showing how to perform source analysis. Scheme is ideal for source analysis, but doesn't give you very many options for exploring the benefits (and weaknesses) of strong typing. Use many languages.
On the other hand, since you're mainly up to methods of programming, I'm not totally sure you need any real language at all. A well defined notation is just as good, and forces your readers to focus on the point you're making rather than the superficial details of one language or another.
我是在 Lisp 和 Scheme 的陪伴下长大的，并且很喜欢它们。 我认为它们是从头开始学习的很棒的语言。 但是，我不确定具有一定编程经验的人会接受这些语言。 如果你的书名中有“Scheme”，你在亚马逊上不会获得很多点击量。 :)
C# 是一种非常容易学习的语言，它拥有快速深入了解并发等主题所需的所有基础知识。 它具有更多的适用性，因为您也可以针对 OO 和 Web 概念。 它也相当受欢迎，你会让公司为员工的书籍付费，这总是有利于销售（“Be a Kick Ass C# Programmer”在费用报销表上比“Modern Lisp Concurrency”走得更远）。
F# 是一门有趣的语言。 它具有Lisp 或Scheme 的功能之美（虽然不完全是，但差不多），并且它使您能够深入研究OOP 主题，并且如果您想让事情变得有趣，还可以连接到.NET Framework 的UI 内容。 但现在，它还很模糊。
我无法使用 Ruby，所以就个人而言，我会硬着头皮选择 C#。
I grew up on Lisp and Scheme and love them both. I think they are great languages to learn from scratch on. But, I'm not sure someone with some programming experience would take to those languages. You're not going to get a lot of hits on Amazon for your book with Scheme in the title. :)
C# is a very easy language to learn and it's got all the basics you would need to dive into topics like concurrency pretty quickly. It has more applicability because you can target OO and web concepts as well. It's also fairly popular and you would get companies paying for their employees books which is always good for sales ("Be a Kick Ass C# Programmer" goes much further on an expense reimbursement sheet than "Concurrency in Modern Lisp").
F# is an interesting language. It's got the functional beauty of a Lisp or Scheme (well not quite, but almost) and it gives you some ability to dive into OOP topics as well as hook into the .NET Framework for UI stuff if you want to spice things up. But, right now, it's obscure.
I can't speak to Ruby, so personally, I would bite the bullet and go with C#.
老实说，我不能为此推荐 Ruby。 当我在商业世界中进行日常编程时，我非常喜欢它，当然比 C 或 Java 更喜欢它。 但它的语义定义如此不明确，以至于我对它的信任度不如 C 的一半，尽管我可能会花几个小时争论一个声明并查阅取代 K&R 的厚得多的白皮书，但我还是得出结论：最后相当确信，如果我有一个合格的编译器（是的，我知道，我是一个梦想家，但在这里和我一起工作）我知道另一边会发生什么。
Ruby 在很多方面都很出色，但就任何正式的事情而言，两者永远不会见面。
我自己倾向于投票给 Haskell，因为每次我转身时，我都会惊讶于该语言定义中的一切都有多么有意义。 （尽管承认只花了一年左右的时间，我确信我什至还没有探索过 Haskell 98 的一半角落。）
而且我也理解 Dikjstra 与函数式的事情； 回去阅读他的论文，他非常处于一个命令式的世界； 我没有资格说他是否真的走错了路。 也许我只是对他的写作和他的思想感到惊讶。 但这似乎确实让他很高兴，那么使用 Algol 60 怎么样？ ？
Honestly, I can't recommend Ruby for this. When I program day-to-day in my commercial world, I like it quite a lot, certainly much more than C or Java. But the semantics of it are so ill-defined that I don't trust it half as much as C where, though I may spend several hours arguing over a statement and consulting that much thicker white book that replaced K&R, I come out in the end fairly convinced that if I've got a conforming compiler (yes, I know, I'm a dreamer, but work with me here) I know what's coming out the other side.
Ruby is wonderful in many ways, but as far as anything formal goes, the twain will never meet.
I'd tend to vote for Haskell myself, because every time I turn around I'm amazed at how much sense everything makes in that language definition. (Though admittedly after only a year or so at it, I'm sure I've not explored half the corners of even Haskell 98.)
And I understand, too, the Dikjstra vs. functional thing; going back and reading his papers he's very much in an imperative world; I am not qualified to say whether he really went the wrong way there. Perhaps I'm just overwhelmed by how good his writing is, as much as his thought. But it did seem to please him, so what about using Algol 60?
这是个好主意。
我认为Scheme是一个不错的选择，因为它允许人们以最少的必需品将不同的抽象付诸实践（以库的形式）。
从方案转换为验证系统（如 PVS）也很容易（http://pvs.csl.sri。 com/）
干杯
That's a nice idea.
I think Scheme is a good option as it allows one to put into practice(in the form of libraries) different abstractions with a bare minimum essentials.
It is also easy to translate from scheme to a verification system like PVS (http://pvs.csl.sri.com/)
cheers
我认为你自己应该对你的书所使用的语言有相当多的经验，或者有人熟练地审查你的代码。
就我个人而言，我会使用 Common Lisp，因为我对此很熟悉，而且它是实现任何概念的绝佳语言。 其他选项可能是 Erlang、Haskell、Ruby 或 Python，甚至可能是某种 ML 方言。 我对C家族（包括C#和Java）有偏见，他们似乎停留在较低层次的概念思考上。
I think that you should yourself have quite some experience in the language you use for your book, or someone proficient to review your code.
Personally, I'd use Common Lisp, since I am familiar with that, and it's a great language to implement any concept. Other options might be Erlang, Haskell, Ruby, or Python, perhaps even some ML dialect. I am biased against the C family (including C# and Java), they seem stuck to a lower level of thinking about concepts.
有相当多的大学使用 Perfect Developer 来教授形式化方法（免责声明：我与该产品有联系）。 它是围绕表达规范、数据细化和算法的语言构建的。 它有一个用于验证的自动定理证明器，以及一个可以生成 C++、C# 和 Java 的代码生成器。 PD 的设计很大程度上受到“编程学科”的启发，但是我们发现这种表示法对于大型系统来说相当不切实际，因此该表示法与 Dijktra 的表示法有所不同。
There are quite a few universities using Perfect Developer for teaching formal methods (disclaimer: I am connected with this product). It is built around a language for expressing specifications, data refinement and algorithms. It has an automatic theorem prover for verification, and a code generator that can produce C++, C# and Java. The design of PD was very much inspired by "A Discipline of Programming", however we found the notation rather impractical for large systems, so the notation has diverged somewhat from Dijktra's.