Open 2020.02.06
IT技術とCoqの世界 -- 「証明」=「プログラム」=「計算」の意味を考える #1

IT技術とCoqの世界 -- 「証明」=「プログラム」=「計算」の意味を考える (後半)

  • このエントリ
ーをはてなブックマークに追加
1123
2471
タグ :

■ 動画紹介

詳細
プログラマーは考える。プログラミングは論理的である

Coqは、一般には「証明支援システム」と呼ばれています。多くのIT技術者にとって、Coqは、特殊な分野(数学の問題の証明等)での特殊なコンピュータの利用だという印象を与えるかもしれません。
ただ、Coqにできることと、IT技術者が日常的に行っていることとの間には、実は、大きな共通点があります。

あらためて確認したいのは、IT技術者にとって一番身近な対象であるプログラムが、極めて「論理的」な性格を持つということです。プログラミングするときに、
我々は営業トークやプレゼンをする時とは違った頭を使います。
それは端的に言って、「論理的」に考えるということだと思います。プログラムの「意図」を、プログラマは論理的にコードとして実装します。

プログラマーは機械と対話する。人間の「意図」を伝えるために

そのことは、IT技術者にとって、プログラミングと並んで一番身近な活動である、テストやデバッグがどういう活動かを考えてみてもよくわかります。テストでは、
簡単なデータを与えてプログラムが予想通り(それは、「意図」に対して論理的に正しく)動いているかをチェックします。
デバッグは、予想とは異なる振る舞いをするプログラムを、「意図」に照らして論理的に見直すことに他なりません。

コンピュータの側からみると、コンピュータは、ハードのエラーがない限り、与えられたプログラムのコードを忠実に実行します。コンピュータにとって、
そのプログラムが実現すべき「意図」というのは、コードそのものによって与えられます。それ以外の手段で、コンピュータに人間の意図を伝える方法はありません。

プログラムのバグやエラーというものに、コンピュータには責任はありません。基本的な問題は、人間が、その意図を実現するように、コンピュータにコードを与えたかという問題です。

プログラマーは悩む。「仕様」と「実装」の間で

プログラミングでの人間の「意図」は、コードでの「実装」とは区別して「仕様」と呼ばれています。プログラムの開発で、仕様と実装を一致させる必要があります。そのために有効ないろいろな方法が、経験に基づいて提案されています。「テスト・デバッグ・ソースリーディング」のサイクルの繰り返しは、そうした経験的なノウハウの典型的な例です。

Coqが注目されているのは、まさに、この仕様と実装の一致のチェックに、人間のプログラマでなくコンピュータを使おうというところにあります。

難しそうな数式を使った数学と、プログラマが無意識のうちにでも従うプログラムのロジックとは、違ったもののように思われるかもしれませんが、その「論理性」についていえば、両者は同じものです。

仕様が形式的に定義されていれば、あるコードがその仕様の忠実な実装であるかは、形式的に証明できるはずです。Coqは、そうした開発スタイルを可能にします。

■ コンテンツ一覧

視聴条件:コンテンツ一覧の動画はご購入することで全て視聴できます。


■講師・スピーカー紹介

丸山 不二夫
東京大学教育学部卒業。一橋大学大学院社会学研究科博士課程修了。稚内北星学園大学学長、早稲田大学大学院情報生産システム研究科客員教授等を歴任。オープンソースのコミュニティ活動に積極的に参加。日本Javaユーザー会名誉会長。日本Androidの会名誉会長。クラウド研究会代表。 近年では、日本のIT業界がグローバルな技術イノベーションの一翼を担うことを目標に、連続講演会「マルレク」を主宰し、クラウドコンピューティングや人工知能などの技術について講演を行っている。

丸山事務所(マルレク):  http://www.digital-life365.com/
日本Androidの会:   https://www.android-group.jp/
過去の講演資料:    https://goo.gl/XM5YsT

2016 年9月更新

  • このエントリ
ーをはてなブックマークに追加

関連動画