Home | Notifications | New Note | Local | Federated | Search | Logout

Note Detail

きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-05-27 21:36:47)
新しい型チェッカーとして話題になっているRubyのRigorというソフトウェア。少なくとも現状の私の理解の範囲ではあんまり聞いていていい気持ちにならない…。
テストにかかれている情報を型推論に使うということだけど、それは存在命題の証明を得ているということであり、矛盾の存在を証拠にコード上のバグを検出できるということに価値はあると思う。
でも型システムとして一般に期待することは全称命題を型システムが証明してくれていることだと思うので、「型チェッカー」と聞いて期待するものと違いすぎるように思う。仮にこのような仕組みが「Rubyの型チェッカー」として広まるようなことがあれば、型チェッカーという言葉の価値が毀損されてしまうのではないか…。
これが「セマンティックなLinter」みたいなキャッチフレーズであったら何も思わなかったかもしれない。