Conversation

Notices

1. きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Thursday, 17-Jun-2021 20:11:15 JST きゅーけー

   SICP 会中にすごいアイデアを思いついてしまった。いままで Guile で ACL2 のコードを書くことばかり考えてたけど、逆も可能だ。Guile のコードから ACL2 で解釈可能な可能な限り等価なコードを生成して ACL2 で証明すればいい。こっちの方が簡単だし、まさに私のやりたいことだ。

   • きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Thursday, 17-Jun-2021 22:07:27 JST きゅーけー

     in reply to

     これは無理な気がしてきた。