小島＠福井コンピュータです．
コメント頂き，有難う御座います．
>「何かに全ての仕様を盛り込む」ことは可能だと思います。ただ、それが
>ソースプログラムより記述しやすかったり、わかりやすくなったりは
>しないというだけでしょう。
大変興味深いので，もう少し御教授願えませんでしょうか．
# 例えば，具体的にはどういう場合でしょうか．
(先に申しましたように)「仕様の定義次第」と云う気がしないでもない
ので，以下私の考えを補足しておきます．
私は，「このアプリケーションと全く同じものを作ってくれ」のような
無理矢理なケースや，正しさを完全に証明出来る程小さいプログラムは
別として，現実的な開発において，
・暗黙的な仕様が存在する．仕様自体を全て明示することが出来ない．
よって，何かによって仕様に関する情報が完全に共有されることがない．
・「何か」が仕様を完全に網羅出来ているかどうかを確認する方法がない為，
「何かに全ての仕様が盛り込まれた」状況が確認されることがない．
# ソース プログラムであれ，実行コードであれ，其の他の文書であれ，
# 其の中に完全に仕様が網羅されることは無い．
と云う気がしています．