24/04/08 21:06:18.84 7R4dahmI.net
カリーハワード対応では、命題と型が対応し、その型をもつ値を構築することが証明になるそうだ
プログラミングにおいてライブラリ関数などを使う際は、引数と戻り値の意味だけ知っていればよく、実装は読まなくてもいい
ここから類推するに、数学も命題の意味が分かっていれば証明を読む必要は無いのではないか？
24/04/08 21:06:18.84 7R4dahmI.net
カリーハワード対応では、命題と型が対応し、その型をもつ値を構築することが証明になるそうだ
プログラミングにおいてライブラリ関数などを使う際は、引数と戻り値の意味だけ知っていればよく、実装は読まなくてもいい
ここから類推するに、数学も命題の意味が分かっていれば証明を読む必要は無いのではないか？