ATS は静的型のプログラミング言語で、形式的な仕様で統一されています。 ATS には2つのサブ言語があります: 1つ目は仕様記述のためのもので、2つ目は実装を記述するためのものです。 さらに、実装がその仕様に一致しているか証明するための定理証明サブシステムもあります。 もし ATS についてたった一つだけ単語を持ち出すとすれば、 それは 精密 (precision) でしょう。 ATS でのプログラミングとは明確であろうとすることであり、 そして可能なかぎり精密さを強制することです。 このテーマはこの本の中で何度も具体的に説明します。
ソフトウェアを明確に作成するためには、 そのソフトウェアがどのような動作を期待されているのか明記しなければなりません。 今日において、ソフトウェアの仕様 (ここでの用法はあいまいですが) はしばしば形式主義の一種として扱われています。 その形式主義は、UML のようなモデリング言語の図表を使った議論を通じた表現から、VDM や Z のような形式的仕様を記述する文字列による表現まで幅があります。 しばしばソフトウェアの仕様の主な目的とは、チーム中の開発者間で相互理解を得ることです。 ソフトウェアの仕様を得た後、プログラミング言語によって仕様を実装する必要があります。 一般的に、実装が現実的にその仕様を満たしているかどうか合理的に信頼するのは非常に難しいものです。 当初は実装が仕様と首尾一貫している場合でさえ、 ソフトウェアが進化するにつれて仕様との乖離はほぼ不可避です。 このような乖離によるひどい結果はとてもなじみ深いものでしょう。 実装が徐々にそれ自身の仕様に変貌していく中でソフトウェアの振舞いを理解しなければならないために、 仕様に対する信頼は損なわれます。 開発者にとっては、ソフトウェアを保守/拡張することはより危険で困難になります。 ユーザにとっては、 ソフトウェアを使ったり学習したりすることに時間と労力が要求されるようになります。
もともとは数学的な土台として Martin-Loef によって作られた型理論を参考に、 仕様と実装を一つのプログラミング言語として結びつける試みとして、私は ATS をデザインしました。 ATS には静的な要素と動的な要素があります。 直観的に、静的な要素と動的な要素はそれぞれ型とプログラムを扱います。 特に仕様は静的な要素です。 ある仕様が与えれたとき、 どうやってその仕様 (型) に一致した実装になっているかを確認すれば良いのでしょうか？ その立証のために、私達は実装を行なうプログラマに ATS の定理証明サブシステムを使った証明も行なうことを要請します。 これはプログラマを中心にすえたプログラムの検証方法です。 強調すると、私達はプログラムの検証にプログラマ中心のアプローチをしています。
プログラミング言語としての ATS は豊かな構文と高機能を両立しています。 ATS は多様なプログラミングパラダイムをサポートしています。 関数型プログラミング、命令型プログラミング、並列プログラミング、モジュラープログラミング、などです。 けれども ATS のコアは値渡し (call-by-value) の関数型言語に基づいていて、驚くほど単純です。 そしてこの本が ATS プログラミングへの旅のスタートです。 この本では主に高品質なプログラムを作成することを容易にする ATS における多様なプログラミングの機能について、例を通して使い方を説明します。 またプログラミングの理論よりもプログラミングのやり方に焦点をあてます。 もしあなたが主に ATS の型理論の基礎に興味があるのであれば、他の文献をおすすめします。
実装ができるのであれば、あなたは "良いプログラマ" です。 "より良いプログラマ" であるためには、あなたの実装について説明できるべきです。 もしあなたがあなたの実装が仕様に一致するか保証できるなら、 あなたは間違いなく "もっとも良いプログラマ" でしょう。 ATS の学習があなたを "もっとも良いプログラマ" になるための素晴しい探検の旅につれていくことを願っています。 さあ、旅をはじめましょう!