《Daisuke Okanohara / 岡野原…

jrf> 《Daisuke Okanohara / 岡野原 大輔さん:X:2025-10-19》  
https://x.com/hillbig/status/1979865923873124704
＞これに加えて人が全部のコードを見きれないという自体に向けて、従来からある形式的検証など、そのプログラムの動作を保証する手法が改めて注目されるだろうし、プログラミング言語自体もAIに合わせたものを作っていかなければいけない＜

なるほど。すべての科学理論をコンピュータ定理証明できるようにしたい…といったら、昔は鼻で笑われるか、敵意を向けられたのだけど(電気回路を推論から作るとか夢でしかなかったし)、プログラムを形式的検証するというのは、AI だからこそ苦行に耐えれて、効率的になるというのは「確かに」と思う。