戻る

こう、動的型付き言語に静的型付き言語を埋め込むような感じで、未証明のプログラム中に直観主義論理で証明可能なものや一階述語論理で証明可能なものをシームレスに埋め込めると嬉しいのかもしれないけど

そういう「部分的な強い保証を埋め込みたい」みたいなの本当に様々な属性について言えて、たとえば C++ や Rust であっても「実行時に一切の副作用が発生しない純粋な関数である」みたいな属性を与えたかったりするわけですね。これはあまりに定番なので constexpr や const fn として表明できるよう言語仕様が用意されたわけだけど

あるいは「この関数は実行時に絶対に panic しない」とか「この関数はメモリアロケーションしない」とか「この関数は I/O を行わない」とか、マジで埋め込みたい保証が無限にあるんだわ