これは一種の奇妙な質問です。形式手法を使ったプログラミングの学習に関する本を書いている最中です。プログラミングの経験がある人を対象にしています。アイデアは、彼らに高品質のプログラマーになるように教えることです。
基本的な表記法は、いくつかの並行性と通信の拡張機能とともに、ダイクストラのプログラミングの分野からのものになります。
EWDとは異なり、最終的には生徒に実際の実行可能プログラムを作成してもらいたいと思います。つまり、ある時点でEWD表記から他の言語に翻訳することを意味します。私が最初に正式なプログラミングを始めたとき、私はCをターゲットにしましたが、多くの配管を書くことになります。さらに、ポインターの処理などの複雑さがすべてあります。Rubyは、SchemeやLispと同様に、明らかに可能なターゲットです。しかし、さまざまな機能言語もあります。私は特に並行性に興味があるので、Erlangは可能性のようです。
それで、最後に、私の質問があります：彼らの正式に開発されたプログラムをターゲットにするために、私は私の読者にどの言語を教えるべきですか？
あなたの好きな プログラミング 言語の答えは何かという明白な答えを無視して、私は 2 つの有用な答えを見ることができます:
一方では、中級プログラマーと思われる人にメソッドをデモンストレーションしようとしています。単一の言語を選択して、それを本の言語として祝福すると、何らかの理由でその言語を好まない潜在的な読者を遠ざける可能性があります. メソッドをデモンストレーションしているので、たまたま要点を簡潔に説明する言語でスニペットを使用する余裕があります。たとえば、RIIA のデモンストレーションに使用できる唯一の言語はおそらく C++ ですが、この同じ言語は、ソース分析の実行方法を示すには不十分です。スキームはソース分析には理想的ですが、厳密な型指定の利点 (および欠点) を調べるためのオプションはあまり多くありません。多くの言語を使用します。
一方で、あなたは主にプログラミングの方法に取り組んでいるので、実際の言語がまったく必要かどうかは完全にはわかりません。明確に定義された記法も同様に優れており、読者はある言語の表面的な詳細ではなく、作成しているポイントに集中する必要があります。
私は Lisp と Scheme で育ち、どちらも大好きです。ゼロから学ぶのに最適な言語だと思います。しかし、ある程度のプログラミング経験のある人がそれらの言語を受け入れるかどうかはわかりません。タイトルに「Scheme」が含まれている本は、Amazon であまりヒットしないでしょう。:)
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 に取って代わったはるかに分厚い白い本を参照したりするのに数時間を費やすことはあるかもしれませんが、私が適合するコンパイラを持っていれば (はい、私は夢想家ですが、ここで私と一緒に仕事をします)、反対側から出てくるものを知っているとかなり確信しています。
Ruby は多くの点で素晴らしいですが、形式的なことに関して言えば、この 2 つが出会うことはありません。
私自身、Haskell に投票する傾向があります。なぜなら、振り向くたびに、その言語定義のすべてがどれほど理にかなっているのかに驚かされるからです。(確かに、わずか 1 年かそこらで、私は Haskell 98 の隅々まで探索したことがないと確信しています。)
また、Dikjstra と関数型の違いも理解しています。戻って彼の論文を読んでいると、彼は非常に命令的な世界にいます。彼が本当にそこで間違った道を進んだかどうかを言う資格はありません。おそらく私は、彼の考えと同じくらい彼の文章がいかに優れているかに圧倒されているだけです. しかし、それは彼を喜ばせたようだったので、Algol 60を使用するのはどうですか?
本で使用する言語についてかなりの経験があるか、コードをレビューするのに熟達した人が必要だと思います。
個人的には、Common Lisp を使い慣れているので、Common Lisp を使用します。Common Lisp は、あらゆる概念を実装するのに最適な言語です。他のオプションは、Erlang、Haskell、Ruby、または Python である可能性があり、おそらくいくつかの ML の方言でさえあります。私は C ファミリー (C# や Java を含む) に偏見を持っています。
いいアイデアですね。私はSchemeが良い選択肢だと思います.Schemeは、最小限の必需品でさまざまな抽象化を(ライブラリの形で)実践できるからです. スキームから PVS ( http://pvs.csl.sri.com/ )のような検証システムへの変換も簡単です。
乾杯
形式的な方法を教えるために Perfect Developer を使用している大学はかなりあります (免責事項: 私はこの製品に関係しています)。仕様、データの改良、およびアルゴリズムを表現するための言語を中心に構築されています。検証用の自動定理証明機能と、C++、C#、および Java を生成できるコード ジェネレーターがあります。PD の設計は「A Discipline of Programming」に大いに影響を受けましたが、この表記法は大規模なシステムでは実用的ではないことがわかったため、Dijktra の表記法から多少逸脱しています。