プログラミング作法の話

こういうことを考える実際的意味は、十分あるものの、
「正しい」の意味をここまで限定しちゃうと、現実から遠ざかるかも。プログラム正しさとは、人間的、社会的、組織的、技術的文脈が決定するのではないか。そしてそれを実際に役に立つレベルで抽象化することは、もちろんできるだろうけど、それはもっと「プログラム認知科学」、「プログラム社会学」いや、「プログラム経済学」、「プログラム経営理論」とでもいうような体系と文脈の中でしか語れないものなのではないか。

補足。すべてのものごとの意味と価値の源泉は、結局のところ、人間と社会でしかないので。人間とも社会とも切り離された、絶対的な意味も価値も存在しないのだから。コンピュータプログラミングとして、その例外ではない。社会に張りめぐらされた意味と価値の網の目と構造物の中で、どういう位置づけにあるものか、ということが、そのモノの「正しさ」を決定する。だから、そのプログラムをとりまく、実際的な人間と社会の意味と価値の構造を描き出し、そのなかの位置づけを多面的に描き出すことなしに、そのプログラムの「正しさ」について語ることなどできないのではないか。だから、社会学や組織学、経営学のような、人文科学的な理論体系でしか、正しいプログラム、というものを実践的に定義することができないような気がします。

今やっとオリジナルのスライドの方を読みました。なるほど最終的には形式的仕様記述の重要性を説いているわけですね。それを説明するためにある資料群は思考実験的要素が強いかな、と思いました^^;。
少なくともここで言っている「正しいプログラム」は単に「仕様とのずれが無いプログラム」というシンプルな考えで、まったくの正論ですよね。
結局の所「仕様の正しさ」の問題の先の部分に焦点を当てているわけで、ホーア論理式などはシンプルでありながら比較的正確な仕様記述方式だなと思いました。

もちろん「仕様とのずれが無いプログラム」という定義においても、ホーア論理式を書きやすくしたがためにプログラムが読みにくくなるようではなぁ、と思うので、その手法が正しいか否かは留保しますけれど。

検証できることが「正しい」のかどうか…。できないよりは正しいけれど…、といった話ですね。

目的は複数あってどれも落とせない目標だったりすると、それを実現する手法が他の目的の実現を事実上阻害することがたくさんあって、どうやっても綺麗にならない。そうするとある目的だけを見てその理想的実現が成されたからといって「正しい」とはいえない、というのもやはり正論であると思いますです。

社会的に確かめられるのは、
「正しさ」ではなく
「(社会における)価値の有無」なんじゃないでしょうか？

「正しい」ってのは先ず「話の辻褄が合ってる」って意味で、
その話に価値があるかどうかはまた別の次元じゃないかな…

社会的に「正しい」という使い方は私は嫌いでして、そのあたりはこの辺に通じるものがあると思います。
http://www.sk-jp.com/mt/philosophical/archives/2004_06/29_235605.html
上記文脈で言うところの、「ある仕様が存在して、ある実装がその仕様どおり動作すること」を「正しい」と呼ぶのは特に間違いではないとも思います。あくまで「仕様に対して」正しいというだけですけどね^^;。そういう意味で思考実験的だなぁという感想でした。