開発プロセスと不完全性定理と人間の力

読むのが面倒な人は、最後の行だけ読んでください。
ゲーデル不完全性定理によって、完全な開発プロセスを定義することはできないと何回か書いてます。
ゲーデル不完全性定理というのは、要するに「数学が矛盾していないことを証明できない」という定理です。
不完全性定理は数学的な説明を読むと難しいのですが、プログラム的な説明を見るとそこまで難しくありません。
プログラムの完全性を検証するプログラムは、もとのプログラムより少し長くなるので、すべてのプログラムの完全性を検証するプログラムを書くことはできない、という感じです。
不完全性定理無限論の教室 (講談社現代新書)がわかりやすいです。


ただ、ゲーデル不完全性定理には、非常に大切なエピソードがあって
「数学者は、不完全性定理により数学に矛盾のないことを証明できないが、矛盾がないことを知っている」
と話したということです。
証明できる問題に関しても、先に数学者が証明できることがわかってから、証明を進めます。証明するまえから数学者にはわかっているわけです。
同様にプログラムも、組んでから動くかどうかわかるのではなくて、動くことがわかってから組むことの方が多いです。プログラマには、組む前からプログラムが動くことがわかっているのです。


そして、開発プロセスも、うまくいくプロセスを定義することはできないけど、人間にはどのようなプロセスがうまくいくかわかることができて、人間の力によってプロセスをうまくいかせることができます。


じゃあ、人間はどんな力をもっているのか、と。
ここで量子力学です。
量子力学というのは重力と相性がわるくて、重力の理論である相対性理論と統合できていません。
ペンローズは量子重力理論を構築すると途中で計算不可能な過程があらわれると予測しています。
で、人間の脳は、その量子重力の計算不可能な過程を利用して、計算不可能なことを実現しているということです。


つまり、どんな開発プロセスだろうが、人間の力、超重要。