Curry-Howard同型のバグと同等のものは何ですか？

Question

簡単に言えば、Curry-Howard correspondenceは、型が定理であり、この型を返すプログラムが対応する定理の証明であると述べています。

対応は、直観主義計算などの数学的証明の形式化に基づいており、直観主義論理に拘束されています。しかし、数学的証明がそれらの形式言語で書かれているとき、それらの誤りはコンピュータによって検出することができる。たとえば、Mizarは比較的高水準の数学的言語であり、それに書かれた証明書をチェックするコンパイラです。

したがって、Curry-Howardはプログラムをエラーなしで数学的証明に関連付けます。したがって、Curry-Howardは数学的な世界でプログラムバグの概念をどのように翻訳していますか？上記のことによって、それは証明における論理的な誤りではない。

Answer 1

バグのあるプログラムは、プログラムがバグなしで対応するプルーフとは異なる正しいプルーフに対応しています。つまり、バグのあるプログラムは、正しいプルーフに対応しますが、異なるプルーフに対応します。類推すると、あなたの正面玄関から出る特定の一連の手順です。あなたは食料品店への道を歩こうとするかもしれません。おそらくあなたは間違った方向に向かい、理髪店で終わるでしょう。あなたはまだあなたが望むものではなく、道を歩いています。

プルーフの論理エラーは、プログラミング言語のランタイムエラーや構文エラーに似ています。そのような場合、間違ったことを計算したり、証明したり、歩いたりしたわけではありません。あなたは何も計算したり、何かを歩いたり、歩いたりすることができませんでした。私たちの類推では、これは歩く方法と、あなたの左の肘と顎だけを使っていくつかのステップを取ろうとすることを忘れるようなものかもしれません。ステッピングと見なされないものを実行しようとするため、あなたのパス（パスの正否を問わず）を完了することはできません。

あなたが考えるかもしれない興味深い課題 - 可能性のある問題に対して正しくない正しい正しいアルゴリズムを書くこと。