停止問題

大学の授業で停止問題について扱われたことがある。詳細は忘れたが、確か「プログラムが停止するかどうかを検出するプログラムは書けない」ということを数学的帰納法っぽいやり方で証明する、という話だったと思う。
このことを自分で証明した時、ある種の衝撃が走った。当時のぼくは理由がよくわからなかったが、今思えば「実装できない仕様がある」ということに驚いたのかな…
今世の中で起こっていることとは数学的に全く別の次元の話かもしれないが、感覚的には忘れたくない…
仕様の世界にもP≠NPみたいなことってあるんだろうか。ある仕様によって引き起こされる、仕様間の関連や表に見えない仕様を含めた仕様全体の複雑性を知る方法とかあるんだろうか…