お気に入りに登録ならここをクリック！
まとめ
メニューを開く-
coq なんかの証明系で発生を潰せるのってロジック系のバグ限定だよね？ エラーだのバグだのって現実から沸いてくるものだから机上ベースの論理じゃどうしようもないと思うし。証明していこうっていう取り組み自体はいいことだと思ってるんだけど、万能ではないよね？ -
証明を否定するなら同じ論理で静的型チェックも否定されるんですが -
「型システムをバリバリに使ってるから大抵のバグはコンパイル時に検出できる筈」と思ってたら、 == と != の単純なミスに気付かず、意味不明の挙動に悩まされまくった経験ならあります。 -
否定するつもりはさらさらなくて、万能じゃないよね？って言う当たり前の確認です。 「当たり前の確認」っていうのは非常に大切なプロセスです。てか、さっきから対面でイチャついてるカップルいい加減にしろ。
-
個人的に特にこのまわりで気に掛かってるのは型でガチガチに固めるスタイルと証明ってどういう違いがあってどの程度の差があるものなのかなぁと。
-
そもそも現実(宇宙)が魔性によって沸いたモノなんだから、その現実から魔性が沸きまくっても・・・というか、現実は魔性の塊。
-
Content from Twitter
コメント