Event is FINISHED

マルレク 「IT技術とCoqの世界 -- 「証明」=「プログラム」=「計算」の意味を考える 」

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

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

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

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

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

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

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

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

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

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

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

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

Updates
  • タイトル は マルレク 「IT技術とCoqの世界 -- 「証明」=「プログラム」=「計算」の意味を考える 」 に変更されました。 Orig#497441 2019-11-21 22:38:22
More updates
Thu Nov 28, 2019
7:00 PM - 9:00 PM JST
Add to Calendar
Venue
Tickets
一般 SOLD OUT ¥1,500
丸山レクチャーズ会員 FULL
マルレク個人協賛会員 FULL
Venue Address
千代田区神田練塀町3 Japan
Organizer
マルレク
1,216 Followers

[PR] Recommended information