ライスの定理（1953）は、プログラムの非自明な意味的性質は決定不可能であることを証明しています。プログラムが正しいかバグがないかを判定できる一般的なアルゴリズムは存在しません。これは現在のツールの限界ではなく、数学的に確実なことです。