这是一个奇怪的问题。我正在写一本关于学习使用正式方法进行编程的书，并且我将把它针对具有一些编程经验的人。这个想法是教他们成为高质量的程序员。
基本符号将来自 Dijkstra 的Discipline of Programming，以及一些并发和通信扩展。
与 EWD 不同，我希望我的学生最终能够编写出实际的可执行程序。这意味着在某些时候将 EWD 符号转换为其他语言。当我第一次开始进行正式编程时，我的目标是 C，但你最终会编写很多管道，加上处理指针等的所有复杂性。Ruby 显然是一个可能的目标，Scheme 或 Lisp 也是如此。但也有各种功能语言；因为我对并发特别感兴趣，所以 Erlang 似乎是一种可能性。
所以，最后，这是我的问题：我应该教我的读者使用什么语言来定位他们正式开发的程序？
查理，
我一直将 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）
忽略显而易见的你最喜欢的 编程 语言答案是什么，我可以看到两个有用的答案：
一方面，您试图向假定为中级程序员的人演示方法。如果您选择一种语言并祝福它作为您的书籍语言，您可能会疏远那些出于某种原因不喜欢该语言的潜在读者。由于您正在演示方法，因此您可以奢侈地使用恰好能简洁地说明您的观点的语言片段。例如，可用于演示 RIIA 的唯一语言可能是 C++，但这种语言在演示如何执行源代码分析方面非常糟糕。Scheme 是源代码分析的理想选择，但在探索强类型的优点（和弱点）方面没有提供太多选择。使用多种语言。
另一方面，由于您主要掌握编程方法，因此我不完全确定您是否需要任何真正的语言。一个定义明确的符号同样好，它会迫使你的读者关注你正在表达的观点，而不是一种或另一种语言的表面细节。
我是在 Lisp 和 Scheme 上长大的，我喜欢它们。我认为它们是从头开始学习的好语言。但是，我不确定有一些编程经验的人会接受这些语言。标题中包含 Scheme 的书不会在亚马逊上获得很多点击。:)
C# 是一门非常容易学习的语言，它拥有快速深入探讨并发等主题所需的所有基础知识。它具有更多的适用性，因为您也可以针对 OO 和 Web 概念。它也相当受欢迎，你会让公司为他们的员工支付书籍，这些书籍总是有利于销售（“Be a Kick Ass C# Programmer”在费用报销单上比“Concurrency in Modern Lisp”走得更远）。
F# 是一种有趣的语言。它具有 Lisp 或 Scheme 的功能美感（不完全是，但差不多），它使您能够深入研究 OOP 主题，如果您想为 UI 内容增添趣味，还可以连接到 .NET Framework 中。但是，现在，它是模糊的。
我不能和 Ruby 说话，所以就个人而言，我会硬着头皮选择 C#。
老实说，我不能为此推荐 Ruby。当我在我的商业世界中进行日常编程时，我非常喜欢它，当然比 C 或 Java 更喜欢它。但是它的语义是如此不明确，以至于我对它的信任度不如 C 的一半，尽管我可能会花几个小时来争论一个声明并查阅取代 K&R 的那本厚得多的白皮书，但我还是在end 相当确信，如果我有一个符合标准的编译器（是的，我知道，我是一个梦想家，但在这里和我一起工作）我知道另一边会发生什么。
Ruby 在很多方面都很棒，但就任何正式的事情而言，这对双胞胎永远不会相遇。
我自己倾向于投票给 Haskell，因为每次我转身时，我都会惊讶于该语言定义中的一切意义。（虽然承认仅仅过了一年左右，但我敢肯定我什至没有探索过 Haskell 98 的一半角落。）
我也理解 Dikjstra 与功能性的东西；回去阅读他的论文，他非常处于一个命令式的世界中；我没有资格说他是否真的走错了路。也许我只是被他的写作如此之好所震撼，就像他的想法一样。但这似乎让他很高兴，那么使用Algol 60怎么样？
这是个好主意。我认为 Scheme 是一个不错的选择，因为它允许人们将不同的抽象（以库的形式）付诸实践，而只需要最少的基本要素。从方案转换为 PVS 等验证系统也很容易（http://pvs.csl.sri.com/）
干杯
我认为你自己应该对你的书所使用的语言有相当的经验，或者一个精通审查你的代码的人。
就个人而言，我会使用 Common Lisp，因为我对此很熟悉，而且它是实现任何概念的好语言。其他选项可能是 Erlang、Haskell、Ruby 或 Python，甚至可能是一些 ML 方言。我对 C 系列（包括 C# 和 Java）有偏见，他们似乎坚持对概念的较低层次的思考。
有不少大学使用 Perfect Developer 来教授形式化方法（免责声明：我与此产品有关）。它是围绕一种用于表达规范、数据细化和算法的语言而构建的。它有一个用于验证的自动定理证明器，以及一个可以生成 C++、C# 和 Java 的代码生成器。PD 的设计非常受“A Discipline of Programming”的启发，但是我们发现这种表示法对于大型系统来说相当不切实际，因此这种表示法与 Dijktra 的有些不同。