過去に ACL2 では副作用を扱う場合は :program モードにすればいいのかとか言ってたけど、間違ってた。ACL2 はファイル入出力などの副作用を扱う処理についても扱えて定理証明できることを知った。どうやっているのかのロジックは論文を読まないと無理そうで今はその体力はないのでそこまで調べるのは諦める。
ACL2 - Logical-story-of-iohttps://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index-seo.php/ACL2____LOGICAL-STORY-OF-IO