教学编程和形式化方法

Question

这里有一个奇怪的问题。我正在写一本关于学习使用正式方法编程的书，我的目标读者是有一些编程经验的人。我们的想法是教他们成为高质量的程序员。

基本符号将来自Dijkstra的Discipline of Programming，以及一些并发和通信扩展。

与EWD不同的是，我希望我的学生最终能写出实际的可执行程序。这意味着在某种程度上将EWD表示法转换为其他语言。当我第一次开始做正式的编程时，我的目标是C，但你最终写了很多管道，再加上处理指针等的所有复杂性。Ruby显然是一个可能的目标，就像Scheme或Lisp一样。但是也有各种各样的函数语言；因为我对并发特别感兴趣，所以Erlang似乎是一种可能性。

所以，最后，这是我的问题:我应该教我的读者什么语言来针对他们正式开发的程序？

Answer 1

查莉

我一直将Dijkstra的杰作与一种编程模型联系在一起，在该模型中，中心阶段被循环和数组占据。如果你坚持使用Dijkstra (例如，计算最弱的前提条件)，我想你会发现函数式语言并不是一个很好的选择。在使用循环和数组为命令式编程提供良好支持的流行语言中，Python可能是额外负担最少的语言。

这并不是说函数式语言不适合形式方法-它们非常适合-但其风格与Dijkstra大不相同。首选的方法强调计算证明；请参阅Richard Bird关于解决数独(这是一种沉重的挑战)的论文或Richard Bird和Phil Wadler的教科书。

对于并发性，这在很大程度上取决于您相信的并发模型(以及正式方法)。John Reppy的并发ML是一个漂亮的消息传递模型。Erlang也有一个很好的干净的限制性模型。另一方面，使用锁和临界区进行编程非常困难，在这种情况下，使用正式方法可能会有更多好处。

另外两句话可能会对你的背景研究感兴趣：

Greg Nelson是我见过的唯一一位将的方法应用于实际系统的程序员，他在Modula 3中工作。(Greg和Mark Manasse共同编写了Trestle window system。)Modula 3是一种非常好的语言，Digital允许它因无能和无能而消亡。Greg有一篇关于Dijkstra的calculus.

• Gerard的扩展的很好的TOPLAS论文霍尔兹曼的建模语言SPIN直接基于Dijkstra的守卫命令的语言，它也支持并发。它的目的是模型检查，而不是编程，它有一些特性，但它与正式方法有很强的联系，能够对断言进行模型检查真的很棒。任何对正式方法感兴趣的人都会想看看它。

(编辑:这里是Greg Nelson论文的链接，或其中之一。- CRM)

Answer 2

忽略显而易见的what's your favorite programming language answers，我可以看到两个有用的答案：

一方面，您试图向被认为是中级程序员的人演示方法。如果你选择一种语言作为你的图书语言，你可能会疏远那些因为某种原因而碰巧不喜欢这种语言的潜在读者。由于您正在演示方法，因此您可以在恰好简明地说明您的观点的语言中使用代码片段。例如，唯一可用于演示RIIA的语言可能是C++，但同样的语言在显示如何执行源代码分析方面相当差。Scheme是源代码分析的理想选择，但并没有给你太多的选择来探索强类型的优点(和缺点)。使用多种语言。

另一方面，由于您主要掌握编程方法，我不完全确定您是否需要任何真正的语言。一个定义良好的符号也一样好，它会迫使你的读者专注于你的观点，而不是一种或另一种语言的表面细节。

Answer 3

我是在Lisp和Scheme上长大的，我很喜欢它们。我认为它们是很好的从头开始学习的语言。但是，我不确定有一些编程经验的人会喜欢这些语言。如果你的书标题中有Scheme，你在亚马逊上不会有太多的点击量。:)

C#是一种非常容易学习的语言，它提供了快速深入了解并发等主题所需的所有基础知识。它有更多的适用性，因为你也可以针对OO和web概念。它也相当受欢迎，你会得到公司为他们的员工支付书籍的费用，这对销售总是有好处的("Be a Kick Ass C# Programmer“在费用报销单上比”现代Lisp中的并发“走得更远)。

F#是一种有趣的语言。它具有Lisp或Scheme的功能美感(嗯，不完全是，但差不多)，如果你想让事情变得更有趣，它给你提供了一些深入OOP主题的能力，以及钩子到.NET框架的UI东西。但是，现在，它是模糊的。

我不能和鲁比说话，所以就我个人而言，我会咬紧牙关选择C#。