マルレク
By 丸山不二夫 Follow | Public

マルレクは、IT 技術のグローバルな新しい波にフォーカスして、丸山が重要と考えるトピックについて、ベンダー・フリーな立場から、出来るだけ新しい情報を、出来るだけわかりやすく、出来るだけ多くの人に、伝えていくことを目標にしています。これまでのマルレクの取り組みについては、「丸山 講演資料集 」 https://goo.gl/JuuyVK を参照ください。

マルレクで取り上げるトピックの詳細については、丸山のblog 「過去・現在・未来」 https://maruyama097.blogspot.jp/ あるいは、丸山のFacebookページ、https://www.facebook.com/fujio.maru... で、継続的に投稿がなされています。

Announcements
  • 2019/11/18

    11/28 マルレク「Coq入門」のお誘いの文章を書き直しました。 https://coq1.peatix.com/ 「プログラマーは考える。プログラミングは論理的である」 「プログラマーは機械と対話する。人間の「意図」を伝えるために」 「プログラマーは悩む。「... read more 11/28 マルレク「Coq入門」のお誘いの文章を書き直しました。 https://coq1.peatix.com/ 「プログラマーは考える。プログラミングは論理的である」 「プログラマーは機械と対話する。人間の「意図」を伝えるために」 「プログラマーは悩む。「仕様」と「実装」の間で」 お読みください。 ------------------------------------------------- プログラマーは考える。プログラミングは論理的である ------------------------------------------------- Coqは、一般には「証明支援システム」と呼ばれています。多くのIT技術者にとって、Coqは、特殊な分野(数学の問題の証明等)での特殊なコンピュータの利用だという印象を与えるかもしれません。ただ、Coqにできることと、IT技術者が日常的に行っていることとの間には、実は、大きな共通点があります。 あらためて確認したいのは、IT技術者にとって一番身近な対象であるプログラムが、極めて「論理的」な性格を持つということです。プログラミングするときに、我々は営業トークやプレゼンをする時とは違った頭を使います。それは端的に言って、「論理的」に考えるということだと思います。プログラムの「意図」を、プログラマは論理的にコードとして実装します。 ------------------------------------------------- プログラマーは機械と対話する。人間の「意図」を伝えるために ------------------------------------------------- そのことは、IT技術者にとって、プログラミングと並んで一番身近な活動である、テストやデバッグがどういう活動かを考えてみてもよくわかります。テストでは、簡単なデータを与えてプログラムが予想通り(それは、「意図」に対して論理的に正しく)動いているかをチェックします。デバッグは、予想とは異なる振る舞いをするプログラムを、「意図」に照らして論理的に見直すことに他なりません。 コンピュータの側からみると、コンピュータは、ハードのエラーがない限り、与えられたプログラムのコードを忠実に実行します。コンピュータにとって、そのプログラムが実現すべき「意図」というのは、コードそのものによって与えられます。それ以外の手段で、コンピュータに人間の意図を伝える方法はありません。 プログラムのバグやエラーというものに、コンピュータには責任はありません。基本的な問題は、人間が、その意図を実現するように、コンピュータにコードを与えたかという問題です。 ------------------------------------------------- プログラマーは悩む。「仕様」と「実装」の間で ------------------------------------------------- プログラミングでの人間の「意図」は、コードでの「実装」とは区別して「仕様」と呼ばれています。プログラムの開発で、仕様と実装を一致させる必要があります。そのために有効ないろいろな方法が、経験に基づいて提案されています。「テスト・デバッグ・ソースリーディング」のサイクルの繰り返しは、そうした経験的なノウハウの典型的な例です。 Coqが注目されているのは、まさに、この仕様と実装の一致のチェックに、人間のプログラマでなくコンピュータを使おうというところにあります。 難しそうな数式を使った数学と、プログラマが無意識のうちにでも従うプログラムのロジックとは、違ったもののように思われるかもしれませんが、その「論理性」についていえば、両者は同じものです。 仕様が形式的に定義されていれば、あるコードがその仕様の忠実な実装であるかは、形式的に証明できるはずです。Coqは、そうした開発スタイルを可能にします。 show less

Comments