ソフトウェア・エンジニアリングの新しい潮流 -- Deep Specificationの世界
2019/9/24 マルレク
概要：https://deep-spec.peatix.com/
資料ダウンロード：http://bit.ly/2muEmcl
資料viewer
「はじめに」から
小論の目的は、ソフトウェア・エンジニアリングの領域で起きている “Deep Specification” という新しい流れをIT技術者に紹介することである。
第一部では、ソフトウェア・エンジニアリング見直しの背景として、現在の大規模システムの開発がはらむ問題をいくつかとりあげた。
現代では、ITシステムは、社会のあらゆる領域に深く浸透している。大規模システムの開発が、明示的にせよ潜在的にせよかかえる問題が、「バグのない安全なITシステムを社会に提供する」という点で、大きな弱点となる可能性はあると筆者は考えている。セキュリティに関心を持つIT技術者は多いと思う。”Deep Specification” のようなソフトウェア・エンジニアリングの分野で起きている変化にも、関心を持つ人が増えることを期待したい。
第二部では、”Deep Specification” の概略を紹介する。開発にコンピュータの力を借りるのは、当たり前のことなのだが、“Deep Specification” が借りようとしているのは、コンピュータが「論理的＝数学的推論」を正しく行う能力を持っているという、その「力」である。
ここでは、 ”Deep Specification” の取り組みの中で、どのような具体的なプロジェクトが走っているのかの紹介を中心に行った。これらの取り組みは、一見、抽象的で理論的なレベルでの試行に見える。また、その「成果」もリアルにみれば限定的なものだ。ただ、第一部で紹介したいくつかの問題への対応を強く意識しているという点では、現実的で実践的な問題意識にドライブされていることには注意が必要だと思う。
”Deep Specification” のムーブメントは、1980年代にDijkstraらが推進しようとしたコンピュータ・サイエンスへの「形式的手法」の導入を、現代に復活させようとしているものと見ることができる。第三部は、「形式的手法」の方法論的中核である「プログラミングと論理」の関係の認識について触れたものである。ただ紙幅の制限で、40年前の議論の歴史的回顧中心にとどまっている。これについては別の機会に補いたい。
小論では、現代の「形式的手法」の技術的な詳細については、立ち入らなかった。それを理解するには、別の準備が必要だからである。特に、現代の「形式的手法」の Lingua Franca であるCoqの知識は不可欠である。次回のマルレクは、「Coq入門」をテーマにしようと思っている。
小論のテーマは、前回のマルレクの「Yet Another AI （別の人工知能技術）」と内容的につながったものだ。特に前回の第三部「機械による数学的推論は可能か？」とは密接に関係している。今回の問題意識は、その問いのコンピュータ開発自体への適用、「機械によるプログラミングは可能か？」に関わるものである。数学をコンピュータ・プログラムの形で再構成しようとしたVoevdskyらのUniMathの試みと、 ”Deep Specification” の試みが、ほぼ同じ時期に登場したのは偶然ではないのだ。
小論では、あまり理論的な話ができなかったのだが、前回のマルレクのサブゼミ 「型の理論入門」 が、前回と今回、そして次回のマルレク「Coq入門」をつなぐ理論的な背景説明になっている。興味がある方は、ぜひ参照してほしい。
